From 1cf2b12bee7da79c52d840517f56c28b4a5182d0 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 11 May 2020 11:32:20 -0400 Subject: [PATCH] Reverse bit order for cr0 in proof --- src/soc/alu/formal/proof_output_stage.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/soc/alu/formal/proof_output_stage.py b/src/soc/alu/formal/proof_output_stage.py index dc723acd..aa35dd4a 100644 --- a/src/soc/alu/formal/proof_output_stage.py +++ b/src/soc/alu/formal/proof_output_stage.py @@ -70,13 +70,13 @@ class Driver(Elaboratable): o_signed = Signal(signed(64)) comb += o_signed.eq(dut.o.o) # Assert only one of the comparison bits is set - comb += Assert(cr_out[0] + cr_out[1] + cr_out[2] == 1) + comb += Assert(cr_out[3] + cr_out[2] + cr_out[1] == 1) with m.If(o_signed == 0): - comb += Assert(cr_out[2] == 1) - with m.Elif(o_signed > 0): comb += Assert(cr_out[1] == 1) + with m.Elif(o_signed > 0): + comb += Assert(cr_out[2] == 1) with m.Elif(o_signed < 0): - comb += Assert(cr_out[0] == 1) + comb += Assert(cr_out[3] == 1) # Assert that op gets copied from the input to output -- 2.30.2