invert test condition in formal proof of ALU output stage

diff --git a/src/soc/alu/formal/proof_output_stage.py b/src/soc/alu/formal/proof_output_stage.py
index aa35dd4a3bfe65623d2aeabf281929d9b9d6a686..288da07170b9c46bc52e38d1e728e10e835b47e3 100644 (file)
--- a/src/soc/alu/formal/proof_output_stage.py
+++ b/src/soc/alu/formal/proof_output_stage.py
@@ -74,9 +74,19 @@ class Driver(Elaboratable):
         with m.If(o_signed == 0):
             comb += Assert(cr_out[1] == 1)
         with m.Elif(o_signed > 0):
-            comb += Assert(cr_out[2] == 1)
+            # sigh.  see https://bugs.libre-soc.org/show_bug.cgi?id=305#c61
+            # for OP_CMP we do b-a rather than a-b (just like ADD) and
+            # then invert the *test condition*.
+            with m.If(rec.insn_type == InternalOp.OP_CMP):
+                comb += Assert(cr_out[3] == 1)
+            with m.Else():
+                comb += Assert(cr_out[2] == 1)
         with m.Elif(o_signed < 0):
-            comb += Assert(cr_out[3] == 1)
+            # ditto as above
+            with m.If(rec.insn_type == InternalOp.OP_CMP):
+                comb += Assert(cr_out[2] == 1)
+            with m.Else():
+                comb += Assert(cr_out[3] == 1)
 
 
         # Assert that op gets copied from the input to output