Concurrent assertions describe behavior that spans over simulation time and are evaluated only at the occurrence of a clock tick.
SystemVerilog concurrent assertion statements can be specified in a module, interface, or program block, running concurrently with other statements. Here are the properties of a concurrent assertion:
- The test expression is evaluated at clock edges, based on values in sampled variables
- Sampling of variables happens in the preponed region, and evaluation of the expression happens in the observed region of the simulation scheduler
- It can be placed in a procedural, module, interface, or program block
- It can be used in both dynamic (simulation) and formal verification techniques
10 min read | Intermediate Level
What You'll Learn
- The defining properties of a concurrent assertion: when it's evaluated, and where it can be used
- Why the preponed region determines exactly which value of a signal gets checked on a given clock edge
- How changing just the boolean expression inside the same
assert propertyproduces completely different pass/fail behavior - How to read the "Offending" annotation in a failed assertion's log output
Example #1: AND
Two signals a and b are driven at positive clock edges with random values. The assertion checks that both signals are expected to be high at every positive edge of the clock for the entire simulation — it should fail for every instance where either a or b is found to be zero:
module tb;
bit a, b;
bit clk;
always #10 clk = ~clk;
initial begin
for (int i = 0; i < 10; i++) begin
@(posedge clk);
a <= $random;
b <= $random;
$display("[%0t] a=%0b b=%0b", $time, a, b);
end
#10 $finish;
end
// This assertion runs for entire duration of simulation
// Ensure that both signals are high at posedge clk
assert property (@(posedge clk) a & b);
endmodule
The assertion is executed on every positive edge of clk and evaluates the expression using values of the variables in the preponed region — a delta cycle before the given clock edge. So if a changes from 0 to 1 on the same edge that clk goes from 0 to 1, the value of a taken for the assertion is still zero, because that's what it was just before the clock edge.
Assertion fails for all cases where either a or b is found zero, since the expression is expected to be true for the entire duration of the simulation:
| Time (ns) | a | b | Result |
|---|---|---|---|
| 10 | 0 | 0 | FAIL |
| 30 | 0 | 1 | FAIL |
| 50 | 1 | 1 | PASS |
| 70 | 1 | 1 | PASS |
| 90 | 1 | 0 | FAIL |
| 110 | 1 | 1 | PASS |
| 130 | 0 | 1 | FAIL |
| 150 | 1 | 0 | FAIL |
| 170 | 1 | 0 | FAIL |
| 190 | 1 | 0 | FAIL |
Output
Compiler version P-2019.06-1; Runtime version P-2019.06-1; Dec 11 14:46 2019 [10] a=0 b=0 testbench.sv", 24: tb.unnamed$$_4: started at 10ns failed at 10ns Offending '(a & b)' [30] a=0 b=1 "testbench.sv", 24: tb.unnamed$$_4: started at 30ns failed at 30ns Offending '(a & b)' [50] a=1 b=1 [70] a=1 b=1 [90] a=1 b=0 "testbench.sv", 24: tb.unnamed$$_4: started at 90ns failed at 90ns Offending '(a & b)' [110] a=1 b=1 [130] a=0 b=1 "testbench.sv", 24: tb.unnamed$$_4: started at 130ns failed at 130ns Offending '(a & b)' [150] a=1 b=0 "testbench.sv", 24: tb.unnamed$$_4: started at 150ns failed at 150ns Offending '(a & b)' [170] a=1 b=0 "testbench.sv", 24: tb.unnamed$$_4: started at 170ns failed at 170ns Offending '(a & b)' [190] a=1 b=0 "testbench.sv", 24: tb.unnamed$$_4: started at 190ns failed at 190ns Offending '(a & b)' $finish called from file "testbench.sv", line 14. $finish at simulation time 200
Quick Check
Q: Suppose a was driven with a plain blocking assignment instead of <=, and happened to change from 0 to 1 in the exact same delta cycle as a clock edge. Would the assertion see the new value (1) or the old value (0)?
Show Answer
The old value (0). Assertions sample in the preponed region, which captures values as they stood just before the clock edge — regardless of exactly how or when a value changes elsewhere in that same time step, the assertion only ever sees what was true immediately prior to the edge it's evaluating on.
Example #2: OR
The same testbench, but the property now checks that at least one of the two signals is high on every clock instead of requiring both:
module tb;
bit a, b;
bit clk;
always #10 clk = ~clk;
initial begin
for (int i = 0; i < 10; i++) begin
@(posedge clk);
a <= $random;
b <= $random;
$display("[%0t] a=%0b b=%0b", $time, a, b);
end
#10 $finish;
end
// This assertion runs for entire duration of simulation
// Ensure that atleast 1 of the two signals is high on every clk
assert property (@(posedge clk) a | b);
endmodule
| Time (ns) | a | b | Result |
|---|---|---|---|
| 10 | 0 | 0 | FAIL |
| 30 | 0 | 1 | PASS |
| 50 | 1 | 1 | PASS |
| 70 | 1 | 1 | PASS |
| 90 | 1 | 0 | PASS |
| 110 | 1 | 1 | PASS |
| 130 | 0 | 1 | PASS |
| 150 | 1 | 0 | PASS |
| 170 | 1 | 0 | PASS |
| 190 | 1 | 0 | PASS |
Output
Compiler version P-2019.06-1; Runtime version P-2019.06-1; Dec 11 15:13 2019 [10] a=0 b=0 testbench.sv", 24: tb.unnamed$$_4: started at 10ns failed at 10ns Offending '(a | b)' [30] a=0 b=1 [50] a=1 b=1 [70] a=1 b=1 [90] a=1 b=0 [110] a=1 b=1 [130] a=0 b=1 [150] a=1 b=0 [170] a=1 b=0 [190] a=1 b=0 $finish called from file "testbench.sv", line 14.
Only the very first cycle (10ns, where both are 0) fails — the exact same random stimulus as Example #1, but a dramatically different pass/fail pattern, purely from swapping & for | in the property itself.
Quick Check
Q: Using the identical stimulus, at 90ns (a=1, b=0), Example #1's AND property failed. Why does Example #2's OR property pass at that same moment?
Show Answer
Because a | b only needs one of the two to be true, and a is 1 — that alone satisfies the OR condition, even though b is 0. The AND property required both to be true, which b=0 violates.
Example #3: XOR (Written as a Negated XNOR)
The property expression is modified once more, this time to !(!a ^ b):
module tb;
bit a, b;
bit clk;
always #10 clk = ~clk;
initial begin
for (int i = 0; i < 10; i++) begin
@(posedge clk);
a <= $random;
b <= $random;
$display("[%0t] a=%0b b=%0b", $time, a, b);
end
#10 $finish;
end
// This assertion runs for entire duration of simulation
// Ensure that atleast 1 of the two signals is high on every clk
assert property (@(posedge clk) !(!a ^ b));
endmodule
| Time (ns) | a | b | Expression !(!a ^ b) | Result |
|---|---|---|---|---|
| 10 | 0 | 0 | 0 | FAIL |
| 30 | 0 | 1 | 1 | PASS |
| 50 | 1 | 1 | 0 | FAIL |
| 70 | 1 | 1 | 0 | FAIL |
| 90 | 1 | 0 | 1 | PASS |
| 110 | 1 | 1 | 0 | FAIL |
| 130 | 0 | 1 | 1 | PASS |
| 150 | 1 | 0 | 1 | PASS |
| 170 | 1 | 0 | 1 | PASS |
| 190 | 1 | 0 | 1 | PASS |
Output
Compiler version P-2019.06-1; Runtime version P-2019.06-1; Dec 11 15:26 2019 [10] a=0 b=0 "testbench.sv", 24: tb.unnamed$$_4: started at 10ns failed at 10ns Offending '(!((!a) ^ b))' [30] a=0 b=1 [50] a=1 b=1 "testbench.sv", 24: tb.unnamed$$_4: started at 50ns failed at 50ns Offending '(!((!a) ^ b))' [70] a=1 b=1 "testbench.sv", 24: tb.unnamed$$_4: started at 70ns failed at 70ns Offending '(!((!a) ^ b))' [90] a=1 b=0 [110] a=1 b=1 "testbench.sv", 24: tb.unnamed$$_4: started at 110ns failed at 110ns Offending '(!((!a) ^ b))' [130] a=0 b=1 [150] a=1 b=0 [170] a=1 b=0 [190] a=1 b=0 $finish called from file "testbench.sv", line 14. $finish at simulation time 200
Working through the boolean algebra, !(!a ^ b) simplifies to exactly a != b — in other words, this convoluted-looking expression is just an XOR(a, b) check written a longer way. Checking every row of the table above confirms it: the property passes precisely on the cycles where a and b differ, and fails on every cycle where they match.
Quick Check
Q: Given that !(!a ^ b) is equivalent to a != b, what single, simpler operator could replace the entire expression?
Show Answer
a ^ b (plain XOR) — ^ is already true exactly when its two operands differ, which is exactly what the longer, double-negated expression computes.
Where Are Simple Boolean Concurrent Assertions Used?
Lightweight, single-cycle boolean checks like these are a common sanity-check layer sitting alongside more complex protocol-sequence assertions — checking things like "request and acknowledge should never differ for more than a cycle" or "these two mutually-exclusive control signals should never both be high at once," every single clock, for the entire run.
Common Beginner Mistakes
Mistake #1: Assuming a concurrent assertion samples the current (post-edge) value
As Example #1 explains, sampling happens in the preponed region — the value as it stood just before the clock edge. Why? A signal that changes in the same delta cycle as the clock edge won't be seen as changed by the assertion on that specific edge; it'll be picked up on the next one instead.
Mistake #2: Forgetting concurrent assertions work for formal verification too
Unlike immediate assertions, which are simulation-only, concurrent assertions can be used in both dynamic (simulation) and formal verification. Why? This is exactly why concurrent assertions are the foundation formal tools build on — their clock-based, declarative structure translates directly into something a formal solver can reason about.
Mistake #3: Writing an unnecessarily complex boolean expression
As the third example shows, !(!a ^ b) and a ^ b are functionally identical, but one is far easier to read at a glance. Why? A property that's hard to read is harder to trust during a code review — simplifying an expression algebraically before writing it into an assertion is worth the extra minute.
Mistake #4: Assuming "Offending" always names one specific signal
In these examples, the "Offending" annotation names the entire boolean expression, since that's the whole of what's being checked. Why? For more complex, multi-part sequences (covered in SystemVerilog Assertions and the articles that follow), the same annotation instead names whichever specific piece of the sequence actually broke — it's worth reading carefully rather than assuming it always means the same thing.
Practice Exercise
Challenge: Predict a NAND Property
Using the exact same stimulus sequence from Example #1 (10ns: a=0,b=0; 30ns: a=0,b=1; 50ns: a=1,b=1; 90ns: a=1,b=0), predict the pass/fail result at each of those four times for the property assert property (@(posedge clk) !(a & b)); (NAND).
Hint
!(a & b) is true whenever a and b are not both 1 — it only fails when both are simultaneously high.
Solution
10ns (0,0): PASS — not both high. 30ns (0,1): PASS — not both high. 50ns (1,1): FAIL — both are high, which is the one case NAND forbids. 90ns (1,0): PASS — not both high. NAND is the exact opposite of the AND property from Example #1 — it fails only where AND would have passed.
Summary
In this tutorial, you learned:
- A concurrent assertion is evaluated at every occurrence of a clock edge, using values sampled in the preponed region — just before that edge
- Concurrent assertions can be used in modules, interfaces, or programs, and work for both simulation and formal verification
- Swapping the boolean operator inside an otherwise identical
assert propertycan completely change which cycles pass or fail against the same stimulus - A complex-looking boolean expression can often be simplified algebraically —
!(!a ^ b)is justa != bin disguise - The "Offending" annotation in a failure log names whatever specific part of the checked expression actually caused the failure
