Add assertions for output stage cr0

diff --git a/src/soc/alu/formal/proof_output_stage.py b/src/soc/alu/formal/proof_output_stage.py
index 50fc4e49c754ed3098c825ec806ca2a690a74901..dc723acdad873bd1df02fb460353542150226f3b 100644 (file)
--- a/src/soc/alu/formal/proof_output_stage.py
+++ b/src/soc/alu/formal/proof_output_stage.py
@@ -1,7 +1,7 @@
 # Proof of correctness for partitioned equal signal combiner
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 
 # Proof of correctness for partitioned equal signal combiner
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 

-from nmigen import Module, Signal, Elaboratable, Mux, Cat
+from nmigen import Module, Signal, Elaboratable, Mux, Cat, signed

 from nmigen.asserts import Assert, AnyConst, Assume, Cover
 from nmigen.test.utils import FHDLTestCase
 from nmigen.cli import rtlil
 from nmigen.asserts import Assert, AnyConst, Assume, Cover
 from nmigen.test.utils import FHDLTestCase
 from nmigen.cli import rtlil


@@ -64,6 +64,20 @@ class Driver(Elaboratable):
         with m.Else():
             comb += Assert(dut.o.o == o)
 
         with m.Else():
             comb += Assert(dut.o.o == o)
 

+        cr_out = Signal.like(cr0)
+        comb += cr_out.eq(dut.o.cr0)
+
+        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)
+        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[0] == 1)
+

 
         # Assert that op gets copied from the input to output
         for p in rec.ports():
 
         # Assert that op gets copied from the input to output
         for p in rec.ports():