A general-purpose Formal correctness test suite is needed for Power ISA, similar in characteristics to bug #194. A good first processor to try testing is Microwatt: https://github.com/antonblanchard/microwatt/ * bug #306 - ALU Proof DONE * bug #331 - Logical Proof DONE * bug #332 - CR Proof DONE * bug #335 - Branch Proof DONE * bug #340 - ShiftRot Proof DONE * bug #418 - SPR Proof DONE * bug #419 - MUL Proof DONE * bug #421 - TRAP Proof DONE proofs for all scalar v3.0B pipelines completed. * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/branch/formal;hb=HEAD * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/alu/formal;hb=HEAD * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/cr/formal;hb=HEAD * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/logical/formal;hb=HEAD * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/mul/formal;hb=HEAD * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/shift_rot/formal;hb=HEAD * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/trap/formal;hb=HEAD * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/fu/spr/formal;hb=HEAD
The Power ISA pipelines are done: ALU, Logical, CR, Branch, Shift, SPR, Mul, Trap - this can be considered completed.