From 02318eaee9983dad92ab4c0ef76febc562a198cc Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Thu, 14 May 2020 17:39:45 +0100 Subject: [PATCH] invert test condition in formal proof of ALU output stage --- src/soc/alu/formal/proof_output_stage.py | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) 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 -- 2.30.2