From: Cesar Strauss <cestrauss@gmail.com>
Date: Sat, 1 Oct 2022 22:06:23 +0000 (-0300)
Subject: Avoid toggling go_i when rel_o is low
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=2683a097ed9197507c77e79392c0f318f4ab09ea

Avoid toggling go_i when rel_o is low

This must be enforced on the scoreboard, in its proof.
---

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index f8d6fb0f..85c7f82b 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -103,6 +103,11 @@ class CompALUMultiTestCase(FHDLTestCase):
         m.submodules.dut = dut = MultiCompUnit(regspec, alu, CompALUOpSubset)
         # TODO Test shadow / die
         m.d.comb += [dut.shadown_i.eq(1), dut.go_die_i.eq(0)]
+        # Avoid toggling go_i when rel_o is low (rel / go protocol)
+        rd_go = Signal(dut.n_src)
+        m.d.comb += dut.cu.rd.go_i.eq(rd_go & dut.cu.rd.rel_o)
+        wr_go = Signal(dut.n_dst)
+        m.d.comb += dut.cu.wr.go_i.eq(wr_go & dut.cu.wr.rel_o)
         # Transaction counters
         do_issue = Signal()
         m.d.comb += do_issue.eq(dut.issue_i & ~dut.busy_o)
@@ -110,7 +115,7 @@ class CompALUMultiTestCase(FHDLTestCase):
         m.d.sync += cnt_issue.eq(cnt_issue + do_issue)
         # Ask the formal engine to give an example
         m.d.comb += Cover(cnt_issue == 2)
-        self.assertFormal(m, mode="cover", depth=4)
+        self.assertFormal(m, mode="cover", depth=10)
 
 
 if __name__ == "__main__":