From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 11 May 2020 15:32:20 +0000 (-0400)
Subject: Reverse bit order for cr0 in proof
X-Git-Tag: div_pipeline~1278
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1cf2b12bee7da79c52d840517f56c28b4a5182d0;p=soc.git

Reverse bit order for cr0 in proof
---

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