From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 5 Nov 2023 14:18:40 +0000 (-0300)
Subject: Allow the formal engine to perform a same-cycle result in the ALU
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=HEAD;ds=sidebyside

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.
---

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()