X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Fexperiment%2Fformal%2Fproof_compalu_multi.py;h=d81f35e12151518a77a2bf5358016acef9c7952c;hb=e3654a3502e0770d7af2fb168ef016a6a398b233;hp=fd3a50f0e8c469e9cc5bfed483937294c825f60c;hpb=e33da1093516e48b93bd7a0807658e5cd9f90d1c;p=soc.git

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index fd3a50f0..d81f35e1 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -101,14 +101,60 @@ class CompALUMultiTestCase(FHDLTestCase):
         # Instantiate "random" ALU
         alu = ALU()
         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)
+        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)
         cnt_issue = Signal(4)
         m.d.sync += cnt_issue.eq(cnt_issue + do_issue)
+        do_read = Signal(dut.n_src)
+        m.d.comb += do_read.eq(dut.cu.rd.rel_o & dut.cu.rd.go_i)
+        cnt_read = []
+        for i in range(dut.n_src):
+            cnt = Signal(4, name="cnt_read_%d" % i)
+            m.d.sync += cnt.eq(cnt + do_read[i])
+            cnt_read.append(cnt)
+        do_write = Signal(dut.n_dst)
+        m.d.comb += do_write.eq(dut.cu.wr.rel_o & dut.cu.wr.go_i)
+        cnt_write = []
+        for i in range(dut.n_dst):
+            cnt = Signal(4, name="cnt_write_%d" % i)
+            m.d.sync += cnt.eq(cnt + do_write[i])
+            cnt_write.append(cnt)
+        do_alu_write = Signal()
+        m.d.comb += do_alu_write.eq(alu.p.i_valid & alu.p.o_ready)
+        cnt_alu_write = Signal(4)
+        m.d.sync += cnt_alu_write.eq(cnt_alu_write + do_alu_write)
+        do_alu_read = Signal()
+        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)
+            m.d.sync += cnt.eq(cnt + (do_issue & dut.rdmaskn[i]))
+            cnt_masked_read.append(cnt)
+
         # Ask the formal engine to give an example
-        m.d.comb += Cover(cnt_issue == 2)
-        self.assertFormal(m, mode="cover", depth=4)
+        m.d.comb += Cover((cnt_issue == 2)
+                          & (cnt_read[0] == 1)
+                          & (cnt_read[1] == 0)
+                          & (cnt_write[0] == 1)
+                          & (cnt_write[1] == 1)
+                          & (cnt_alu_write == 1)
+                          & (cnt_alu_read == 1)
+                          & (cnt_masked_read[0] == 1)
+                          & (cnt_masked_read[1] == 1))
+        self.assertFormal(m, mode="cover", depth=10)
 
 
 if __name__ == "__main__":