From: Cesar Strauss <cestrauss@gmail.com>
Date: Tue, 15 Nov 2022 11:52:58 +0000 (-0300)
Subject: Keep the valid signal from the formal engine ALU stable, until read
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=a4bde05025e6583c49942c05c4caaee0e12c1768

Keep the valid signal from the formal engine ALU stable, until read
---

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