From: Cesar Strauss <cestrauss@gmail.com>
Date: Sat, 8 Oct 2022 20:36:39 +0000 (-0300)
Subject: Add write transaction counter
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=263c9a85f9a9b344fc0c277210ca4d0576d82674

Add write transaction counter
---

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index 87662340..10a27fe7 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -120,11 +120,20 @@ class CompALUMultiTestCase(FHDLTestCase):
             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)
 
         # Ask the formal engine to give an example
         m.d.comb += Cover((cnt_issue == 2)
                           & (cnt_read[0] == 1)
-                          & (cnt_read[1] == 0))
+                          & (cnt_read[1] == 1)
+                          & (cnt_write[0] == 1)
+                          & (cnt_write[1] == 1))
         self.assertFormal(m, mode="cover", depth=10)