Count zero_a and imm_data.ok as masked read transactions

[soc.git] / src / soc / experiment / formal / proof_compalu_multi.py

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index fc3ce637bc0ebbbab37469caa65eabbbfa0500e9..8f75b7b070f8ae783cf14d9ceaa6ad7fb50ad0ea 100644 (file)
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -35,7 +35,7 @@ https://bugs.libre-soc.org/show_bug.cgi?id=197
 import unittest
 
 from nmigen import Signal, Module
-from nmigen.hdl.ast import Cover
+from nmigen.hdl.ast import Cover, Const
 from nmutil.formaltest import FHDLTestCase
 from nmutil.singlepipe import ControlBase
 
@@ -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)
@@ -135,15 +138,28 @@ class CompALUMultiTestCase(FHDLTestCase):
         m.d.comb += do_alu_read.eq(alu.n.o_valid & alu.n.i_ready)
         cnt_alu_read = Signal(4)
         m.d.sync += cnt_alu_read.eq(cnt_alu_read + do_alu_read)
+        cnt_masked_read = []
+        for i in range(dut.n_src):
+            cnt = Signal(4, name="cnt_masked_read_%d" % i)
+            if i == 0:
+                extra = dut.oper_i.zero_a
+            elif i == 1:
+                extra = dut.oper_i.imm_data.ok
+            else:
+                extra = Const(0, 1)
+            m.d.sync += cnt.eq(cnt + (do_issue & (dut.rdmaskn[i] | extra)))
+            cnt_masked_read.append(cnt)
 
         # 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)
-                          & (cnt_alu_read == 1))
+                          & (cnt_alu_read == 1)
+                          & (cnt_masked_read[0] == 1)
+                          & (cnt_masked_read[1] == 1))
         self.assertFormal(m, mode="cover", depth=10)