Temporal operators come in weak and strong pairs. A weak operator lets a still-pending obligation pass at end of evaluation, while a strong one fails it.
Only pure s_eventually defers purely to the end. s_until, s_until_with, and s_nexttime can all fail mid-trace, before the end.
Weak | Strong | Question answered | Simulation note |
|---|---|---|---|
|
| Does | Only the weak form is unbounded; |
|
| Does | Only the strong form is unbounded ( |
|
| Does | Strong form needs the next tick to exist |
|
| Must | Weak forgives a |
|
| Must | Same, plus the overlap tick |
Nothing: weak operators forgive pending obligations at end of evaluation. The strong flavor would fail instead.
Each diagram shows one stimulus and the verdict of every attempt, tick by tick. A signal row is the value sampled at that edge.
Two attempts, one pass and one fail. nexttime looks at a single future tick and nothing else.
always has no end of its own: one low p fails the attempt, and a p that stays high is never reported as a pass during the run.
A pending strong obligation is neither pass nor fail yet. If gnt never came, both attempts would fail at the end of the run.
The listing below is not run in this course's checks because Verilator 5.048 does not support s_until_with, s_eventually or property always.
// not-run: Verilator 5.048 does not support s_until_with, s_eventually or property always
// Assumes busy, handoff, start, done, both_high are design signals.
property p_hold;
@(posedge clk) $rose(busy) |-> busy until handoff;
endproperty
property p_hold_strong;
@(posedge clk) $rose(busy) |-> busy s_until_with handoff;
endproperty
property p_live;
@(posedge clk) start |-> s_eventually done;
endproperty
property p_inv;
@(posedge clk) always (!both_high);
endpropertyp until q needs p at every tick before the first q, excluding the q tick. until_with includes that tick, so one overlapping cycle decides between them.
Slot 0: busy 0, done 0. Idle.
Slot 1: busy rises. Both obligations start watching.
Slot 2: busy 1. Holding.
Slot 3: busy 1. Holding.
Slot 4: done 1, busy 0. until passes since the q tick is excluded, while until_with fails here.
Slot 5: both 0. Idle.
The verdict rows show it per attempt: until ends successfully at the done tick, while until_with also needs busy at that tick and fails.
Safety says nothing bad ever happens, and any violation shows in a finite prefix. Liveness says something good eventually happens, and its violation is an infinite behavior.
Finite traces cannot conclude liveness. For simulation sign-off, bound it: s_eventually x becomes ##[1:MAX] x, which turns the check into safety.
Property | Kind | Simulation | Formal |
|---|---|---|---|
Never two grants | Safety | Catches violations | Proves |
Every request granted | Liveness | Pending-at-end heuristic only | Finds starvation loops |
Grant within MAX cycles | Bounded liveness | Catches violations | Proves |
A safety violation has a finite witness: the bad thing happened at some tick. A liveness violation is an infinite behavior, which no finite trace exhibits.
The bench runs both until flavors as real assertions on the slot-4 stimulus from the diagram, then on two more episodes: busy held through the done tick, and a planted early drop. A bounded check stands in for s_eventually, which Verilator 5.048 does not support.
module tb_impl_until;
logic clk = 0;
always #5 clk = ~clk;
logic busy = 0, done = 0, start = 0, fin = 0;
int until_fails = 0, with_fails = 0, bounded_fails = 0;
ap_until: assert property (@(posedge clk) $rose(busy) |-> busy until done) else until_fails++;
ap_with: assert property (@(posedge clk) $rose(busy) |-> busy until_with done) else with_fails++;
// Bounded liveness: the simulation form of "start |-> s_eventually fin".
localparam int MAX = 6;
ap_bounded: assert property (@(posedge clk) $rose(start) |-> ##[1:MAX] fin) else bounded_fails++;
// busy for n ticks, then done; overlap keeps busy high on the done tick.
task automatic episode(int n, bit overlap, int gap = 0);
@(negedge clk) busy = 1;
repeat (n - 1) @(negedge clk);
if (gap) begin busy = 0; repeat (gap) @(negedge clk); end
busy = overlap; done = 1;
@(negedge clk) busy = 0; done = 0;
repeat (3) @(negedge clk);
endtask
initial begin
repeat (2) @(negedge clk);
episode(3, 0); // the diagram: busy drops as done rises
$display("busy drops on the done tick: until %0d failures, until_with %0d", until_fails, with_fails);
episode(3, 1); // busy held through the done tick
$display("busy held through done: until %0d failures, until_with %0d", until_fails, with_fails);
episode(3, 0, 1); // planted: busy drops one tick before done
$display("busy drops before done: until %0d failures, until_with %0d", until_fails, with_fails);
@(negedge clk) start = 1; @(negedge clk) start = 0; repeat (3) @(negedge clk); fin = 1; @(negedge clk) fin = 0;
@(negedge clk) start = 1; @(negedge clk) start = 0; // planted: fin never comes
repeat (MAX + 3) @(negedge clk);
$display("bounded ##[1:%0d] fin: %0d failure (the start that never finished)", MAX, bounded_fails);
if (until_fails != 1 || with_fails != 2 || bounded_fails != 1) $fatal(1, "FAIL: %0d %0d %0d", until_fails, with_fails, bounded_fails);
$display("PASS: until forgave the done tick, until_with demanded it, both caught the early drop, and the bounded form caught the missing fin");
$finish;
end
endmodulebusy drops on the done tick: until 0 failures, until_with 1
busy held through done: until 0 failures, until_with 1
busy drops before done: until 1 failures, until_with 2
bounded ##[1:6] fin: 1 failure (the start that never finished)
PASS: until forgave the done tick, until_with demanded it, both caught the early drop, and the bounded form caught the missing finRun with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.
until and until_with gave right verdicts on all three episodes; nexttime, always [m:n], s_until, s_until_with and s_eventually were rejected as unsupported.