Reset and abort: disable iff, accept and reject

Switch rules off during reset with disable iff, cancel or fail one obligation with sync_accept_on and sync_reject_on, and place each so that it cannot hide a bug or invent one.

Lesson: A3.5
Time: 25 min
Runs on: Verilator
Check: 6 questions

The hold rule for stalled beats fired a burst of failures every time a test applied reset in the middle of traffic. The DUT legally drops rvalid when reset arrives, and the rule did not know that. To quiet the noise, someone turned the assertion off for the whole regression, and three months later a real hold violation shipped.

Reset in the middle of a stalled offer

With disable iff (!rst_n), edge 3 cancels the attempt instead of failing it.

disable iff

disable iff (expr) heads a property and switches the whole assertion off while expr is true. An attempt in progress when it becomes true ends as disabled, which is neither a pass nor a failure. Attempts that would start while it is true are disabled too.

The condition is the one exception to sampling. The standard evaluates it with current values, at any time, so it reacts to reset as soon as reset changes.

Disabled, not failedOne lane per request for disable iff (!rst_n) req |-> ##2 gnt.disable iff (!rst_n) req |-> ##2 gntMeasured on Verilator 5.052: one copy of the assertion per lane

attempt startspassfaildisabled by disable iff

Edge 2 · t=15
A request at 15 waits for gnt two edges later.
Edge 4 · t=35
gnt at 35: the attempt passes.
Edge 5 · t=45
A second request at 45 waits for gnt at 65.
Edge 6 · t=55
Reset arrived at 50, between edges 5 and 6. The attempt from 45 was disabled at that moment, and no verdict is ever reported for it.
Edge 9 · t=85
Reset ended at 70. A request at 85 starts a fresh attempt.
Edge 11 · t=105
No gnt at 105, so this attempt fails. Outside reset the rule still checks everything.

Read the lanes as text

req @15, from edge 2 (t=15): passes at edge 4 (t=35).
req @45, from edge 5 (t=45): is disabled between edges 5 and 6.
req @85, from edge 9 (t=85): fails at edge 11 (t=105).

Sampled values, edge 1 to 11: rst_n 1 1 1 1 1 0 0 1 1 1 1; req 0 1 0 0 1 0 0 0 1 0 0; gnt 0 0 0 1 0 0 0 0 0 0 0.

The program behind the lanes

The lanes come from running this program on Verilator 5.052. Each lane is a separate copy of gnt_in_2 that can start only at that lane's edge, so every verdict and its edge are read from that copy's own output.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic rst_n = 1, req = 0, gnt = 0;

  gnt_in_2: assert property (@(posedge clk) disable iff (!rst_n) req |-> ##2 gnt);

  initial begin
    @(negedge clk); req = 1;            // request at 15
    @(negedge clk); req = 0;
    @(negedge clk); gnt = 1;            // granted at 35
    @(negedge clk); gnt = 0; req = 1;   // request at 45
    @(negedge clk); req = 0; rst_n = 0; // reset from 50 to 70
    @(negedge clk);
    @(negedge clk); rst_n = 1;
    @(negedge clk); req = 1;            // request at 85
    @(negedge clk); req = 0;
    @(negedge clk);                     // no grant at 105
    @(negedge clk);
    $finish;
  end
endmodule

default disable iff (!rst_n); in a module gives that guard to every assertion that does not name its own, which keeps long rule lists short and consistent.

Abort one obligation: accept or reject

Sometimes an event should end one obligation rather than switch the rule off. A flush cancels a pending completion; an error makes the burst in progress wrong at once. The abort operators say this inside a property, and their result is a real verdict.

sync_accept_on (c) p ends the evaluation of p with a pass at the first edge where c is sampled true. sync_reject_on (c) p ends it with a failure. Like the rest of the property, c is sampled at the clock edges.

An error rejects the burst in progressOne lane per burst for start |=> sync_reject_on (err) busy[*3].start |=> sync_reject_on (err) busy[*3]Measured on Verilator 5.052: one copy of the assertion per lane

attempt startspassaborted by accept_on or reject_on

Edge 2 · t=15
Burst 1 starts at 15 and needs busy on the next three edges.
Edge 5 · t=45
busy held at 25, 35 and 45: burst 1 passes.
Edge 7 · t=65
Burst 2 starts at 65.
Edge 9 · t=85
err is sampled at 85 while burst 2 runs. The attempt is rejected here, although busy is still high.

Read the lanes as text

start @15, from edge 2 (t=15): passes at edge 5 (t=45).
start @65, from edge 7 (t=65): is aborted at edge 9 (t=85) (rejected).

Sampled values, edge 1 to 15: start 0 1 0 0 0 0 1 0 0 0 0 1 0 0 0; busy 0 0 1 1 1 0 0 1 1 1 0 0 1 1 1; err 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0.

The program behind the lanes

The lanes come from running this program on Verilator 5.052. Each lane is a separate copy of burst_clean that can start only at that lane's edge, so every verdict and its edge are read from that copy's own output.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic start = 0, busy = 0, err = 0, flush = 0, done = 0;

  burst_clean: assert property (@(posedge clk) start |=> sync_reject_on (err) busy[*3]);

  initial begin
    @(negedge clk); start = 1;              // burst 1 starts at 15
    @(negedge clk); start = 0; busy = 1;    // busy at 25, 35, 45
    @(negedge clk); done = 1;               // done at 35
    @(negedge clk); done = 0;
    @(negedge clk); busy = 0;
    @(negedge clk); start = 1;              // burst 2 starts at 65
    @(negedge clk); start = 0; busy = 1; flush = 1;  // flush at 75
    @(negedge clk); err = 1; flush = 0;     // err at 85
    @(negedge clk); err = 0;
    @(negedge clk); busy = 0;
    @(negedge clk); start = 1;              // burst 3 starts at 115
    @(negedge clk); start = 0; busy = 1;
    @(negedge clk);
    @(negedge clk);                         // no done at 135
    @(negedge clk); busy = 0;
    $finish;
  end
endmodule

A flush accepts the pending completionThe same bursts for start |=> sync_accept_on (flush) ##1 done.start |=> sync_accept_on (flush) ##1 doneMeasured on Verilator 5.052: one copy of the assertion per lane

attempt startspassfailaborted by accept_on or reject_on

Edge 2 · t=15
Burst 1 starts at 15 and owes a done at 35.
Edge 4 · t=35
done at 35: pass.
Edge 8 · t=75
Burst 2 starts at 65, then flush is sampled at 75. The obligation is accepted there, so the missing done at 85 is no failure.
Edge 14 · t=135
Burst 3 starts at 115 with no flush and no done at 135: it fails.

Read the lanes as text

start @15, from edge 2 (t=15): passes at edge 4 (t=35).
start @65, from edge 7 (t=65): is aborted at edge 8 (t=75) (accepted).
start @115, from edge 12 (t=115): fails at edge 14 (t=135).

Sampled values, edge 1 to 15: start 0 1 0 0 0 0 1 0 0 0 0 1 0 0 0; flush 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0; done 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0.

The program behind the lanes

The lanes come from running this program on Verilator 5.052. Each lane is a separate copy of done_or_flush that can start only at that lane's edge, so every verdict and its edge are read from that copy's own output.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic start = 0, busy = 0, err = 0, flush = 0, done = 0;

  done_or_flush: assert property (@(posedge clk) start |=> sync_accept_on (flush) ##1 done);

  initial begin
    @(negedge clk); start = 1;              // burst 1 starts at 15
    @(negedge clk); start = 0; busy = 1;    // busy at 25, 35, 45
    @(negedge clk); done = 1;               // done at 35
    @(negedge clk); done = 0;
    @(negedge clk); busy = 0;
    @(negedge clk); start = 1;              // burst 2 starts at 65
    @(negedge clk); start = 0; busy = 1; flush = 1;  // flush at 75
    @(negedge clk); err = 1; flush = 0;     // err at 85
    @(negedge clk); err = 0;
    @(negedge clk); busy = 0;
    @(negedge clk); start = 1;              // burst 3 starts at 115
    @(negedge clk); start = 0; busy = 1;
    @(negedge clk);
    @(negedge clk);                         // no done at 135
    @(negedge clk); busy = 0;
    $finish;
  end
endmodule

Where the abort goes

An abort covers exactly the property it is written in front of. Put it in the consequent, after the implication, and it acts only on attempts that really started a burst.

At the top level, sync_reject_on (err) start |=> busy[*2] covers the antecedent too. Every edge starts an attempt, including the vacuous ones, so an err while the bus is idle rejects the attempt that starts on that edge. The quiz measures that false failure.

Mechanism	Scope	Result when triggered	Condition read
`disable iff (c)`	the whole assertion	disabled: no verdict	current values
`sync_accept_on (c) p`	the property `p`	pass	sampled at edges
`sync_reject_on (c) p`	the property `p`	failure	sampled at edges

Use disable iff for reset, and the abort operators for protocol events.

The asynchronous forms accept_on and reject_on are not covered yet.

Choosing the mechanism

Use disable iff for reset. It also suits any other condition under which the rule has no meaning. A test mode that drives the bus from another source is one example. "No verdict" is the honest answer there.

Use an abort when the event is part of the protocol. A flush or an error is something the DUT must handle, so the attempt should end with a verdict. It is accepted when the obligation is legally cancelled, and rejected when the event itself breaks the rule.

After reset ends, attempts start again at the first edge where the disable condition is false. The second prediction in the quiz counts exactly which attempts survive a reset.

Checking reset itself

A guarded rule switches itself off whenever reset is active, so it can never notice a DUT that ignores reset. Reset needs rules of its own, without a guard: "while reset is asserted, rvalid is low at the next edge" becomes !rst_n |=> !rvalid.

Write the guard with the polarity the DUT really uses: disable iff (!rst_n) for an active-low reset. A guard on the wrong polarity disables the rule everywhere except during reset, the quietest assertion there is. Guard only the rules reset can break; !(full && empty) should hold even in reset. Run the reset rules from time zero, because the first reset of every test is the cheapest place to find a register that powers up wrong.

Try it

Both forms caught the data change during the stall at 85. Only the unguarded form also failed at 55, where reset legally removed a stalled offer; the guarded form treated that attempt as disabled.

Change the guard to disable iff (rst_n), the wrong polarity, and predict both lines.

RUNVerilator · simulator service

Edit the code, then run it

Expected: hold_guarded failed at: 85 hold_unguarded failed at: 55 85

Check yourself

Predict the outputOne clean burst, then an err pulse while the bus is idle. Predict the exact output.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic start = 0, busy = 0, err = 0;
  int fails;
  burst: assert property (@(posedge clk) sync_reject_on (err) start |=> busy[*2])
    else fails++;
  initial begin
    @(negedge clk); start = 1;           // burst at 15
    @(negedge clk); start = 0; busy = 1; // busy at 25 and 35
    @(negedge clk);
    @(negedge clk); busy = 0;
    @(negedge clk); err = 1;             // err at 55, no burst running
    @(negedge clk); err = 0;
    @(negedge clk);
    $display("failures=%0d", fails);
    $finish;
  end
endmodule

Predict the outputreq is high at 15, 25, 35 and 45 and gnt never comes. Reset is asserted at 15 and 25. Predict the exact output.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic rst_n = 1, req = 0, gnt = 0;
  int fails;
  p: assert property (@(posedge clk) disable iff (!rst_n) req |=> gnt)
    else fails++;
  initial begin
    @(negedge clk); req = 1; rst_n = 0;  // reset at 15 and 25
    @(negedge clk);
    @(negedge clk); rst_n = 1;
    @(negedge clk);
    @(negedge clk); req = 0;             // req high at 15, 25, 35, 45
    @(negedge clk);
    $display("failures=%0d", fails);
    $finish;
  end
endmodule

ConceptReset is asserted while an attempt of a disable iff (!rst_n) property is in progress. What is the attempt's result?

It is disabled: neither a pass nor a failureIt passes vacuouslyIt fails, because the consequent was not metIt waits and resumes after reset

Read the waveformdisable iff (!rst_n) v && !r |=> v until_with r checks this trace. What happens to the attempt started at edge 2?

A stall interrupted by reset

Reset is held low across edge 3.

It fails at edge 3, because v droppedIt is disabled at edge 3 by the resetIt passes at edge 5, where r risesIt succeeds vacuously at edge 2

ConceptAfter a request, done is due two edges later, but a flush cancels the request and no done will come. How should the rule handle the flush?

req |=> sync_reject_on (flush) ##1 donereq |=> !flush until donereq |=> sync_accept_on (flush) ##1 donedisable iff (flush) req |=> ##1 done

Spot the bugEach option checks "after start, busy stays high for three edges, and an err during the burst is a failure". An err while the bus is idle is legal. Which option fails on legal traffic?

start |=> (busy && !err)[*3]

start |=> sync_reject_on (err) busy[*3]

start |=> !err throughout busy[*3]

sync_reject_on (err) start |=> busy[*3]

Remember

disable iff makes attempts cut by reset, or started during it, disabled: no pass, no failure.
Its condition uses current values; Verilator 5.052 still needs reset held across a clock edge.
sync_accept_on ends one obligation with a pass, sync_reject_on with a failure, at the edge where the condition is sampled.
Put an abort in the consequent; at the top level it also rejects idle attempts.
Guard only the rules reset can break, with the real polarity, and check reset with unguarded rules.