From cd78bc57b1ac756681f94fe99e80889ffa1530ff Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 31 Oct 2020 15:29:37 -0300 Subject: [PATCH] Check that the read and write counters differ at most by one This will assure there are no dropped work items. --- src/soc/experiment/formal/proof_alu_fsm.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/soc/experiment/formal/proof_alu_fsm.py b/src/soc/experiment/formal/proof_alu_fsm.py index bb83c918..51bc26d5 100644 --- a/src/soc/experiment/formal/proof_alu_fsm.py +++ b/src/soc/experiment/formal/proof_alu_fsm.py @@ -65,6 +65,11 @@ class Driver(Elaboratable): sync += expected.eq(dut_data_i >> dut_shift_i) with m.Else(): sync += expected.eq(dut_data_i << dut_shift_i) + # Check for dropped inputs, by ensuring that there are no more than + # one work item ever in flight at any given time. + # Whenever the unit is busy (not ready) the read and write counters + # will differ by exactly one unit. + m.d.comb += Assert((read_cnt + ~dut.p.ready_o) & 0xF == write_cnt) # check coverage as output data is accepted with m.If(dut.n.ready_i & dut.n.valid_o): # increment read counter -- 2.30.2