From b798c228e694ffee8c1ba371f73cd7ed0b666588 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 8 Oct 2022 18:05:32 -0300 Subject: [PATCH] Add ALU write transaction counter --- src/soc/experiment/formal/proof_compalu_multi.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py index 10a27fe7..cbbe8570 100644 --- a/src/soc/experiment/formal/proof_compalu_multi.py +++ b/src/soc/experiment/formal/proof_compalu_multi.py @@ -127,13 +127,18 @@ class CompALUMultiTestCase(FHDLTestCase): 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) # Ask the formal engine to give an example m.d.comb += Cover((cnt_issue == 2) & (cnt_read[0] == 1) & (cnt_read[1] == 1) & (cnt_write[0] == 1) - & (cnt_write[1] == 1)) + & (cnt_write[1] == 1) + & (cnt_alu_write == 1)) self.assertFormal(m, mode="cover", depth=10) -- 2.30.2