Two thousand cycles late

dbglab's deadlock, B2, is fixed and pinned (the case study tells the hunt). The escape review asks the uncomfortable question. Commit 11 added the bus lock; the only thing that caught the deadlock it made was a watchdog, 2,000 cycles after the fact, in the one test written for back-pressure. What assertion, written with commit 11, would have reported it at the cause, and would it actually run in the simulators this team uses?

What people usually do, and why it fails

The quick answer is an assertion written from the fix: the DMA must not hold `m_lock` in WAIT. It describes one line of one module, so it means nothing after the safe fix (where the fabric ignores lock entirely) and fires on designs that are fine. The other quick answer is a timeout, the CPU gets `ready` within N cycles, which is the watchdog again with a smaller N: it still reports the symptom, and it fires on any slow but correct design.

The method: from the rule, at its home, proven three ways

1. Find the rule the bug broke, as the specification states it. bus_fabric.sv documents lock in one comment: a locked owner keeps the bus for its next beat. So when the fabric keeps a grant, the owner must use it soon. The DMA holding the bus while it waits for the peripheral broke that promise.

2. Put the bound from the design, not from the failure. A DMA chunk spends at most three cycles between beats (POP, LOAD, WAIT), so the next request must come within 4 cycles of the kept response. A bound taken from the spec fires at the cause; a bound taken from the symptom fires at the symptom.

3. Put it where the rule lives. The fabric owns the grant, so the assertion binds into bus_fabric and speaks in its signals: rsp_fire, accept, owner, m_valid.

4. Prove it three ways. It fires on the buggy commit at the cause cycle. It is silent on every fix and on the whole regression. A cover counts its antecedent, so you know when it is passing because nothing happened.

5. Check that the tool checks it. Run each form once where it must fail. The table at the end of this lesson is that run for the three tools installed here.

The picture: four reports of one deadlock

The case study's idle-grant check states a broader rule, so it needs a looser bound and fires at 181. Keep both: the narrow rule fires closer to the cause, the broad one catches causes nobody thought of.

Do it: write it, run it, prove it

The assertion

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

// not-run: needs dbglab's sources and bench; compile it with them in Verilator (command in the Evidence box)
// lock_checks: the rule behind bus_fabric's lock, as concurrent SVA, bound into the fabric.
// The fabric's comment says what lock is for: "a locked owner keeps the bus for its next beat".
// So whenever the fabric keeps the grant at a response, that owner must request again soon:
// a DMA chunk needs at most 3 cycles (POP, LOAD, WAIT) between beats. Verilator only.
`timescale 1ns/1ps
module lock_checks (
  input logic       clk, rst_n,
  input logic [1:0] m_valid,
  input logic       owner, rsp_fire, accept
);
  int unsigned kept = 0;
  a_lock_next_beat: assert property (@(posedge clk) disable iff (!rst_n)
                      rsp_fire && !accept |-> ##[1:4] m_valid[owner])
    else $error("LOCK_NEXT_BEAT cycle=%0d: grant kept for master %0d, no request within 4 cycles",
                dbglab_tb.cycle, owner);
  c_kept: cover property (@(posedge clk) disable iff (!rst_n) rsp_fire && !accept) kept++;
  final $display("LOCK_CHECK: grant kept at %0d responses", kept);
endmodule

bind bus_fabric lock_checks u_lock (.*);

rsp_fire && !accept is the fabric keeping the grant at a response: that is the antecedent, stated in the fabric's own terms, not the DMA's. .* in the bind connects the checker's ports to the fabric's signals of the same names. The cover counts every time the antecedent happens; its action needs --coverage-user in Verilator, as the table below shows.

It fires at the cause

$ ../probes/run-vl-check.sh . ../probes/lock_checks.sv dma_burst_backpressure 1 +verilator+error+limit+100
dbglab: test=dma_burst_backpressure seed=1
[1685000] %Error: lock_checks.sv:14: Assertion failed in dbglab_tb.dut.u_fab.u_lock.a_lock_next_beat: LOCK_NEXT_BEAT cycle=168: grant kept for master 1, no request within 4 cycles
FAIL test=dma_burst_backpressure seed=1 cycle=2165: WATCHDOG: no bus or stream progress for 2000 cycles; cpu_valid=1 cpu_ready=0 cpu_addr=00003008
...

Read it as a bug report. Where: dbglab_tb.dut.u_fab.u_lock, the fabric. When: cycle 168. What: the grant was kept for master 1, the DMA, and it made no request within the 4 cycles the rule allows. The error limit lets the run continue so you can see the watchdog arrive 1,997 cycles later with nothing moves as its only information. At commit 11, the commit that added lock, the result is the same for seeds 1, 2 and 3.

It is silent on the fix, and on everything else

$ cd ../safefix && ../probes/run-vl-check.sh . ../probes/lock_checks.sv dma_burst_backpressure 1
dbglab: test=dma_burst_backpressure seed=1
PASS test=dma_burst_backpressure seed=1 cycles=772 time=7716 ns
LOCK_CHECK: grant kept at 0 responses
$ cd ../pacedfix && ../probes/run-vl-check.sh . ../probes/lock_checks.sv dma_copy 1
dbglab: test=dma_copy seed=1
PASS test=dma_copy seed=1 cycles=1182 time=11816 ns
LOCK_CHECK: grant kept at 157 responses

Then the whole regression, every test with seeds 1 to 3, on five versions of the design:

The random test, seeds 1 to 60 at commit 11, passed every seed with the assertion silent, across 150,122 kept grants. That matters: an assertion that fires on correct traffic gets switched off within a week.

A pass that proves nothing

Look at the safe-fix row again. The assertion passes everywhere, and its cover says the antecedent never happened, not once. That pass carries no information: the fix stopped the fabric keeping grants, so there is nothing left to check. It is still right to keep the assertion, because the next person to add a lock will make the antecedent real again. But in a report, a vacuous pass must be counted separately from a real one, and the cover is how you count it. The assertion debug lessons cover vacuity in depth.

The same rule in Icarus

Icarus 13 does not compile concurrent assertions or bind (see the table), so for the four-state runs the rule is written as clocked code with hierarchical names:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

// not-run: needs dbglab's sources and bench; compile it next to them in Icarus (command in the Evidence box)
// lock_checks_proc: a_lock_next_beat as clocked code for Icarus 13 (no concurrent SVA, no bind).
`timescale 1ns/1ps
module lock_checks_proc;
  int wait_n = 0;                                   // cycles since the grant was kept; 0 = not armed
  logic who;
  always @(posedge dbglab_tb.clk) begin
    if (!dbglab_tb.rst_n) wait_n <= 0;
    else if (wait_n > 0) begin
      if (dbglab_tb.dut.u_fab.m_valid[who]) wait_n <= 0;
      else if (wait_n == 4) begin
        $error("LOCK_NEXT_BEAT cycle=%0d: grant kept for master %0d, no request within 4 cycles",
               dbglab_tb.cycle, who);
        wait_n <= 0;
      end else wait_n <= wait_n + 1;
    end
    if (dbglab_tb.rst_n && dbglab_tb.dut.u_fab.rsp_fire && !dbglab_tb.dut.u_fab.accept) begin
      wait_n <= 1; who <= dbglab_tb.dut.u_fab.owner;
    end
  end
endmodule

$ ../probes/run-probe.sh . ../probes/lock_checks_proc.sv dma_burst_backpressure 1
dbglab: test=dma_burst_backpressure seed=1
ERROR: ../probes/lock_checks_proc.sv:11: LOCK_NEXT_BEAT cycle=168: grant kept for master 1, no request within 4 cycles
FAIL test=dma_burst_backpressure seed=1 cycle=2165: WATCHDOG: no bus or stream progress for 2000 cycles; cpu_valid=1 cpu_ready=0 cpu_addr=00003008

Same cycle, same message. Two versions of one rule are a maintenance cost; checking that both fire at the same cycle on the buggy commit keeps them in step.

What the tools here really check

Each form below was written into a one-module test that must fail at a known cycle (or, for the cover, hit at a known cycle), so a tool that compiles a form and checks nothing is caught too. For example, the range test:

// snippet: f_range.sv, one of the 14 support tests; a rises at c = 3, b only at c = 9, so this must fail at c = 6
  a_p: assert property (@(posedge clk) a |-> ##[1:3] b) else $error("FIRED range c=%0d", c);

So: in Icarus write checks as clocked procedural code (its suggested -gsupported-assertions gave the same syntax error, and crashed on the deferred test); in Verilator any X check is dead code; and Yosys reads the immediate form with $past, as the proof in Proving the Fix used. The silent bind is the dangerous row: a formal run that "passes" because the property was never there.

What the evidence says

The assertion turned a hang reported 2,000 cycles late as nothing moves into a rule violation four cycles after the wrong decision, naming the fabric, the master and the rule, on commit 11's own regression. It stayed silent on 150,122 correct kept grants, and its cover told apart two passes that look identical in a log: the paced fix, where it checked real traffic, and the safe fix, where it checked nothing.

Traps

Related topics

• Part 9 · Fix, Prove, Prevent

• Next: root-cause analysis, done honestly

• Assertions as always-on probes

• Watchdogs and hang detectors

• SystemVerilog: assertion debug