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/
The Power ISA pipelines are done: ALU, Logical, CR, Branch, Shift, SPR, Mul, Trap - this can be considered completed.