An abort operator wraps a property and watches a condition while that property is being evaluated. If the condition becomes true during the evaluation, the result is decided at once: true for the accept forms, false for the reject forms. Otherwise the result is that of the wrapped property (IEEE 1800-2012, 16.12.14; section numbers in this topic refer to the 2012 text, which the 2017 revision carries forward).
Form | Abort result | When the condition is checked |
|---|---|---|
| true | Every simulation time step during the evaluation, using sampled values |
| false | Every simulation time step during the evaluation, using sampled values |
| true | Only at ticks of the property clock, using sampled values |
| false | Only at ticks of the property clock, using sampled values |
The LRM calls the first two asynchronous resets and the sync forms synchronous resets. It also defines the reject forms through the accept forms: reject_on(c) p means not (accept_on(c) not p). Everything you learn about accept_on carries over with the result flipped.
The abort scope is the evaluation of the wrapped property, not the whole assertion. In start |=> sync_accept_on(cancel) valid[*3] the wrapped property starts one tick after start, so a cancel on the start tick itself is outside the scope.
Question | disable iff (c) | accept_on(c) / reject_on(c) |
|---|---|---|
Where it may appear | Once, at the top of the assertion | Anywhere inside a property; may be nested |
Values used | Current values (not sampled) | Sampled values, like any assertion Boolean |
Result when c is true | Attempt is disabled: neither pass nor fail | Attempt passes (accept) or fails (reject) |
Effect on counters | Disabled attempts are not counted as successes | An accepted abort is a vacuous success (16.14.8) |
The counter row matters for sign-off. An attempt rescued by accept_on is vacuous, and a cover statement records vacuous successes separately from real ones (16.14.3). A burst that was always cancelled can leave the assertion with many passes and no real evidence. Pair each abort with a cover of the full, unaborted case.
All five assertions below check start |=> X valid[*3], where X is the abort or nothing. start is high at tick t0, so the wrapped property is evaluated at t1, t2 and t3. Results follow the LRM text; they were not simulated, because no free tool here accepts the operators.
Case A: valid drops on the last beat, c is high at that same tick
tick t0 t1 t2 t3
start 1 0 0 0
valid - 1 1 0
c 0 0 0 1
valid[*3] FAIL at t3
sync_accept_on(c) valid[*3] PASS at t3 (vacuous): abort at the final tick wins
sync_reject_on(c) valid[*3] FAIL at t3
accept_on(c) valid[*3] PASS (vacuous): c is high in the t3 time step
disable iff (c) ... DISABLED: c is high while the attempt is open
Case B: valid is fine, c pulses for 3 ns between t1 and t2
valid[*3] PASS at t3
sync_accept_on / sync_reject_on PASS at t3: no tick sees c high
accept_on(c) valid[*3] PASS (vacuous), decided between t1 and t2
reject_on(c) valid[*3] FAIL, decided between t1 and t2
disable iff (c) ... DISABLED
Case C: valid drops at t2, c is high at t3
valid[*3], every abort form FAIL at t2: the evaluation ended before cCase A uses the rule "when the abort condition occurs at the same time step where the evaluation of the property ends, the abort condition takes precedence" (16.12.14). Case B is the one real difference between the sync and async forms: only the async forms see a pulse that falls between clock ticks. Which time step a simulator reports for that async abort is tool-dependent, so do not build a check on the exact time.
Nesting: nested aborts are evaluated in lexical order, so when two abort conditions become true in the same time step the outermost wins. accept_on(a) reject_on(b) p passes if a and b rise together.
Inside not: not (accept_on(a) p) fails when a fires. The negation inverts the abort result too.
No local variables: an abort condition may not reference local variables or the sequence methods triggered and matched.
Explicit clocks: a sampled value function other than $sampled inside an abort condition must name its clock, for example $rose(stop, @(posedge clk)).
Sync reject is throughout: the LRM gives sync_reject_on(stop) put[->2] and !stop throughout put[->2] as equivalent. Use whichever your tools support.
// not-run: Verilator 5.048 reports "Unsupported: sync_accept_on (in property expression)"; Icarus 13 has no concurrent assertions
// A burst is three beats of valid unless cancel arrives first.
a_burst: assert property (@(posedge clk) disable iff (!rst_n)
start |=> sync_accept_on(cancel) valid[*3]);
// An error flag fails the burst at once, even between ticks; cancel still ends it early.
a_clean: assert property (@(posedge clk)
start |=> reject_on(err_flag) sync_accept_on(cancel) valid[*3]);
// Cover the unaborted case, or the accept_on can hide that no burst ever completed.
c_full: cover property (@(posedge clk) disable iff (!rst_n)
start ##1 (valid && !cancel)[*3]);Because the abort operators do not compile here, the bench below writes start |=> sync_accept_on(cancel) valid[*3] as three properties, one per beat. Beat k can only fail if no cancel was seen on beats 1 to k-1 and, at beat k, cancel is low and valid is low. A cancel on beat k accepts that beat, which matches the final-tick rule. The three antecedents are mutually exclusive, so each failing burst fails exactly one of them.
Two points about the code: the 1-bit OR is written with |, because in our tests Verilator 5.048 missed a failure when || was used after a multi-cycle antecedent; and the bench adds a separate rule that valid drops after a cancel, because accept_on only relaxes a check and never requires the DUT to stop.
// Burst sender: start launches 3 beats of valid; cancel ends a burst early.
module burst_tx (
input logic clk,
input logic rst_n,
input logic start,
input logic cancel,
output logic valid
);
logic [1:0] left;
always_ff @(posedge clk) begin
if (!rst_n) begin
left <= 0;
valid <= 0;
end else if (start && left == 0) begin
left <= 2'd3;
valid <= 1;
end else if (valid && cancel) begin
left <= 0;
valid <= 0;
end else if (left != 0) begin
left <= left - 1;
valid <= (left > 1);
end
end
endmodule
The rewrite was also compared against a cycle-by-cycle model of the sync_accept_on semantics over 400 random cycles; both reported the same 30 failing attempts. Three changes make the bench fail: a DUT that sends only two beats (valid <= (left > 2)) gives 55 failures; a DUT that ignores cancel trips the a_stop rule 14 times; and replacing the three beat properties with plain start |=> valid ##1 valid ##1 valid fails 13 times on the cancelled bursts, which shows the abort really was doing work.
go |=> sync_reject_on(stop) put[->2], stop goes high at the same tick as the second put. Pass or fail?Fail. The second put ends the evaluation in that time step, and an abort condition in the time step where the evaluation ends takes precedence.
sync_accept_on looks at the condition only at clock ticks. A pulse that rises and falls between two ticks is never sampled high at a tick, so only the asynchronous form, which is checked every time step, sees it.