From: Cesar Strauss Date: Sat, 31 Oct 2020 18:29:37 +0000 (-0300) Subject: Check that the read and write counters differ at most by one X-Git-Tag: 24jan2021_ls180~121 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd78bc57b1ac756681f94fe99e80889ffa1530ff;p=soc.git Check that the read and write counters differ at most by one This will assure there are no dropped work items. --- 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