From: Luke Kenneth Casson Leighton Date: Thu, 14 May 2020 16:39:45 +0000 (+0100) Subject: invert test condition in formal proof of ALU output stage X-Git-Tag: div_pipeline~1230 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=02318eaee9983dad92ab4c0ef76febc562a198cc;p=soc.git 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 aa35dd4a..288da071 100644 --- 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