From 8dba511f874f4a1948072e402e24200ba615d158 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 1 Oct 2022 19:08:00 -0300 Subject: [PATCH] Add counter for operand reads --- src/soc/experiment/formal/proof_compalu_multi.py | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py index 85c7f82b..07ff4002 100644 --- a/src/soc/experiment/formal/proof_compalu_multi.py +++ b/src/soc/experiment/formal/proof_compalu_multi.py @@ -113,8 +113,19 @@ class CompALUMultiTestCase(FHDLTestCase): 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) + m.d.sync += cnt_issue.eq(cnt_issue + do_issue) + 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) + # Ask the formal engine to give an example - m.d.comb += Cover(cnt_issue == 2) + m.d.comb += Cover((cnt_issue == 2) + & (cnt_read[0] == 1) + & (cnt_read[1] == 0)) self.assertFormal(m, mode="cover", depth=10) -- 2.30.2