From: Michael Nolan <mtnolan2640@gmail.com>
Date: Fri, 8 May 2020 18:59:45 +0000 (-0400)
Subject: Add assertions for output stage cr0
X-Git-Tag: div_pipeline~1335
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=555594f6b55a2c34b790c38e7252fe256e194f89;p=soc.git

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 50fc4e49..dc723acd 100644
--- 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>
 
-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
@@ -64,6 +64,20 @@ class Driver(Elaboratable):
         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():