Allow the formal engine to perform a same-cycle result in the ALU

[soc.git] / src / soc / experiment / formal / proof_compalu_multi.py

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index 5abd6a43ad1e4857f499259b9ac482f3b374ac65..96b61a2b6a0375d37347a5ba19d675900ef97a40 100644 (file)
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -153,8 +153,13 @@ class CompALUMultiTestCase(FHDLTestCase):
             m.d.sync += cnt.eq(cnt + do_masked_read[i])
             cnt_masked_read.append(cnt)
         # If the ALU is idle, do not assert valid
-        with m.If(cnt_alu_read == cnt_alu_write):
+        with m.If((cnt_alu_read == cnt_alu_write) & ~do_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