and and or exist at both layers with different semantics. Sequence and composes match threads with length rules, while property and is verdict conjunction from a common start tick.
Which layer applies is decided by operand types, silently. Mixed-up expressions compile cleanly and check the wrong thing.
Form | Operands | Meaning |
|---|---|---|
| Sequence, then property | Endpoint-driven obligation with vacuity |
| Properties | Verdict logic from the same start tick |
| Properties | If |
| Boolean plus properties | Branch selected by |
| Boolean plus property | Two-way correspondence from the same tick |
not p holds exactly when p fails. A sequence used as a property holds if any thread matches, so not s requires every thread to fail.
A negated boolean inside a ranged delay stays existential. a |-> ##[1:2] !b passes if b is low on either tick.
Slot 0: a 0, b 0. Idle.
Slot 1: a 1. Two threads start, watching slots 2 and 3.
Slot 2: b 0. The first thread dies, and the boolean form already passes here.
Slot 3: b 1. The second thread matches, so the sequence holds and not fails.
Slot 4: both 0. Idle.
Write never-in-window as not (a ##[1:2] b) or as a |=> (!b)[*2]. Never as a |-> ##[1:2] !b.
The listing below is not run in this course's checks because Verilator 5.048 does not support property if/else. It accepts the not, iff and implies lines.
// not-run: Verilator 5.048 does not support property if/else
// Assumes gnt, req, fast_mode, link_up, cfg_on are design signals,
// and p_stable_link / p_throughput are properties declared nearby.
property p_never_double;
@(posedge clk) not (gnt ##1 gnt);
endproperty
property p_mode_resp;
@(posedge clk) req |->
if (fast_mode) ##1 gnt
else ##[2:4] gnt;
endproperty
property p_pair;
@(posedge clk) cfg_on iff link_up;
endproperty
property p_rel;
@(posedge clk) p_stable_link implies p_throughput;
endpropertyimplies takes properties on both sides with no endpoint shift and no per-match vacuity. |-> takes a sequence antecedent and times the consequent from each match endpoint.
if (e) samples e at the attempt tick, so a mode change mid-obligation does not reselect. e iff p states two-way correspondence from the same tick.
a |-> ##[1:2] !b wrong for absent-in-window?The ranged delay is existential: one low tick on either cycle satisfies it. Absence needs a universal form such as not (a ##[1:2] b).
p implies q require, and how does its timing differ from |->?If p holds from the attempt tick, q holds from that same tick. Both sides are properties, so there is no endpoint shift and no per-match vacuity.
The universal window form in two spellings, then a same-tick implies check. Each bench drives one legal case and one illegal case and counts failures in the else action. The comparison spelling is deliberate: Verilator rejects unary negation inside sequence expressions.
module tb_impl_not;
timeunit 1ns; timeprecision 1ps;
logic clk = 0;
always #5 clk = ~clk;
logic rst_n = 0;
logic a_stim = 0;
logic b_stim = 0;
int univ_fails = 0;
int not_fails = 0;
// Two spellings of "b absent on both ticks after a rises".
a_univ: assert property (@(posedge clk) disable iff (!rst_n)
$rose(a_stim) |-> ##1 (b_stim == 1'b0) ##1 (b_stim == 1'b0))
else univ_fails++;
a_not: assert property (@(posedge clk) disable iff (!rst_n)
not ($rose(a_stim) ##[1:2] b_stim))
else not_fails++;
task automatic window(input logic b1, input logic b2);
a_stim = 1;
@(negedge clk); a_stim = 0; b_stim = b1;
@(negedge clk); b_stim = b2;
@(negedge clk); b_stim = 0;
repeat (2) @(negedge clk);
endtask
initial begin
repeat (2) @(negedge clk);
rst_n = 1;
@(negedge clk);
window(0, 0); // legal: b low on both ticks
window(0, 1); // illegal: one late b
if (univ_fails == 1 && not_fails == 1)
$display("PASS: clean window held; one late b failed both universal spellings once");
else
$fatal(1, "FAIL: univ_fails=%0d not_fails=%0d (expected 1 and 1)", univ_fails, not_fails);
$finish;
end
endmodulePASS: clean window held; one late b failed both universal spellings oncemodule tb_impl_implies;
timeunit 1ns; timeprecision 1ps;
logic clk = 0;
always #5 clk = ~clk;
logic link_ok = 0;
logic [3:0] cnt = 0;
int fails = 0;
// Same-tick relation between two properties: no endpoint shift.
a_rel: assert property (@(posedge clk) link_ok implies (cnt == 4'd8))
else fails++;
initial begin
@(negedge clk);
link_ok = 1; cnt = 4'd8; // 3 ticks that satisfy the relation
repeat (3) @(negedge clk);
link_ok = 0; cnt = 4'd0; // idle ticks raise no obligation
repeat (2) @(negedge clk);
link_ok = 1; cnt = 4'd7; // 1 tick that breaks it
@(negedge clk);
link_ok = 0;
repeat (2) @(negedge clk);
if (fails == 1)
$display("PASS: 3 same-tick checks held, idle ticks raised no obligation, 1 bad tick failed");
else
$fatal(1, "FAIL: fails=%0d (expected 1)", fails);
$finish;
end
endmodulePASS: 3 same-tick checks held, idle ticks raised no obligation, 1 bad tick failedRun 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.
Verilator 5.048 rejected if / else inside a property (Unsupported: property case expression); implies and iff gave right verdicts on a known trace.