X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Fexperiment%2Fformal%2Fproof_compalu_multi.py;fp=src%2Fsoc%2Fexperiment%2Fformal%2Fproof_compalu_multi.py;h=bf6d2615b8142c15561cc63ca946ce718547e227;hb=a4bde05025e6583c49942c05c4caaee0e12c1768;hp=5abd6a43ad1e4857f499259b9ac482f3b374ac65;hpb=c37b1b1bd9e028288b3095401780158ebca01c20;p=soc.git

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index 5abd6a43..bf6d2615 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -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