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 bb83c9187d69c73a624079e605b42c40f16b7fb4..51bc26d535bf56ebd075afcee8293dd855dc1ad6 100644 (file)
--- 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