From a4bde05025e6583c49942c05c4caaee0e12c1768 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Tue, 15 Nov 2022 08:52:58 -0300 Subject: [PATCH] Keep the valid signal from the formal engine ALU stable, until read --- src/soc/experiment/formal/proof_compalu_multi.py | 5 +++++ 1 file changed, 5 insertions(+) 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 -- 2.30.2