From c37b1b1bd9e028288b3095401780158ebca01c20 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Fri, 28 Oct 2022 10:15:34 -0300 Subject: [PATCH] Check that exactly one ALU write is made, per instruction --- .../experiment/formal/proof_compalu_multi.py | 23 +++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py index 6364a515..5abd6a43 100644 --- a/src/soc/experiment/formal/proof_compalu_multi.py +++ b/src/soc/experiment/formal/proof_compalu_multi.py @@ -139,6 +139,7 @@ class CompALUMultiTestCase(FHDLTestCase): cnt_alu_read = Signal(4) m.d.sync += cnt_alu_read.eq(cnt_alu_read + do_alu_read) cnt_masked_read = [] + do_masked_read = Signal(dut.n_src) for i in range(dut.n_src): cnt = Signal(4, name="cnt_masked_read_%d" % i) if i == 0: @@ -147,13 +148,16 @@ class CompALUMultiTestCase(FHDLTestCase): extra = dut.oper_i.imm_data.ok else: extra = Const(0, 1) - m.d.sync += cnt.eq(cnt + (do_issue & (dut.rdmaskn[i] | extra))) + m.d.comb += do_masked_read[i].eq(do_issue & + (dut.rdmaskn[i] | extra)) + m.d.sync += cnt.eq(cnt + do_masked_read[i]) cnt_masked_read.append(cnt) # If the ALU is idle, do not assert valid with m.If(cnt_alu_read == cnt_alu_write): m.d.comb += Assume(~alu.n.o_valid) - # Invariant check + # Invariant checks + # For every instruction issued, at any point in time, # each operand was either: # 1) Already read @@ -165,6 +169,21 @@ class CompALUMultiTestCase(FHDLTestCase): cnt_read[i] + cnt_masked_read[i] + dut.cu.rd.rel_o[i]) m.d.comb += Assert(sum_read == cnt_issue) + # For every instruction, either: + # 1) The ALU is executing the instruction + # 2) Otherwise, execution is pending (alu.p.i_valid is high) + # 3) Otherwise, it is waiting for operands + # (some dut.cu.rd.rel_o are still high) + # 4) ... unless all operands are masked, in which case there is a one + # cycle delay + all_masked = Signal() + m.d.sync += all_masked.eq(do_masked_read.all()) + sum_alu_write = Signal(4) + m.d.comb += sum_alu_write.eq( + cnt_alu_write + + (dut.cu.rd.rel_o.any() | all_masked | alu.p.i_valid)) + m.d.comb += Assert(sum_alu_write == cnt_issue) + # Ask the formal engine to give an example m.d.comb += Cover((cnt_issue == 2) & (cnt_read[0] == 1) -- 2.30.2