From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 9 Oct 2022 10:08:13 +0000 (-0300)
Subject: Don't issue while busy
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=e3654a3502e0770d7af2fb168ef016a6a398b233

Don't issue while busy

Otherwise, the formal engine, in some cases, will happily assert issue_i
while busy_o is high. MultiCompUnit can't handle that.
---

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index 4e15462b..d81f35e1 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -103,6 +103,9 @@ 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)]
+        # Don't issue while busy
+        issue = Signal()
+        m.d.comb += dut.issue_i.eq(issue & ~dut.busy_o)
         # 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)
@@ -144,7 +147,7 @@ class CompALUMultiTestCase(FHDLTestCase):
         # Ask the formal engine to give an example
         m.d.comb += Cover((cnt_issue == 2)
                           & (cnt_read[0] == 1)
-                          & (cnt_read[1] == 1)
+                          & (cnt_read[1] == 0)
                           & (cnt_write[0] == 1)
                           & (cnt_write[1] == 1)
                           & (cnt_alu_write == 1)