From 263c9a85f9a9b344fc0c277210ca4d0576d82674 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 8 Oct 2022 17:36:39 -0300 Subject: [PATCH] Add write transaction counter --- src/soc/experiment/formal/proof_compalu_multi.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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) -- 2.30.2