From 2a66fe18cd77dd5533c65930d1b241cf6faac455 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 5 Nov 2023 11:18:40 -0300 Subject: [PATCH] Allow the formal engine to perform a same-cycle result in the ALU This adds an exception to holding o_valid low, when the ALU is idle. If a write to the ALU just occurred, allow o_valid to become high, in the same cycle. --- src/soc/experiment/formal/proof_compalu_multi.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py index bf6d2615..96b61a2b 100644 --- a/src/soc/experiment/formal/proof_compalu_multi.py +++ b/src/soc/experiment/formal/proof_compalu_multi.py @@ -153,7 +153,7 @@ 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() -- 2.30.2