Keep the valid signal from the formal engine ALU stable, until read master
authorCesar Strauss <cestrauss@gmail.com>
Tue, 15 Nov 2022 11:52:58 +0000 (08:52 -0300)
committerCesar Strauss <cestrauss@gmail.com>
Tue, 15 Nov 2022 11:55:02 +0000 (08:55 -0300)
src/soc/experiment/formal/proof_compalu_multi.py

index 5abd6a43ad1e4857f499259b9ac482f3b374ac65..bf6d2615b8142c15561cc63ca946ce718547e227 100644 (file)
@@ -155,6 +155,11 @@ class CompALUMultiTestCase(FHDLTestCase):
         # If the ALU is idle, do not assert valid
         with m.If(cnt_alu_read == cnt_alu_write):
             m.d.comb += Assume(~alu.n.o_valid)
+        # Keep ALU valid high, until read
+        last_alu_valid = Signal()
+        m.d.sync += last_alu_valid.eq(alu.n.o_valid & ~alu.n.i_ready)
+        with m.If(last_alu_valid):
+            m.d.comb += Assume(alu.n.o_valid)
 
         # Invariant checks