if statements and $display calls scattered through a testbench — has to be built and maintained by hand for every single rule your design must follow. An assertion lets you state that rule once, declaratively, and have the simulator check it continuously for the entire run, flagging a violation the exact clock cycle it happens rather than leaving you to notice a wrong output much later.The behavior of a system can be written as an assertion that should be true at all times. Assertions are used to validate the behavior of a system defined as properties, and can also be used in functional coverage.
12 min read | Intermediate Level
What You'll Learn
- What a design "property" is, and the two ways a property can be violated
- Why a declarative assertion scales better than the equivalent checker logic written by hand
- The four types of assertion statements:
assert,assume,cover, andrestrict - How a
sequenceand apropertyrelate to each other, and the steps to building a complete assertion
What Are Properties of a Design?
If a property of the design that is being checked for by an assertion does not behave in the expected way, the assertion fails. For example, assume the design requests a grant and expects to receive an ack within the next four cycles. But if the design gets an ack on the fifth cycle instead, the property that an ack should be returned within four clocks is violated, and the assertion fails.
If a property of the design that is being checked for by an assertion is forbidden from happening, the assertion also fails. For example, assume a small processor decodes instructions read from memory, encounters an unknown instruction, and results in a fatal error. If such a scenario is never expected from the design, the property that only valid instructions can be read from memory is violated, and the assertion fails.
As evident from both examples, properties of a given design are checked for by writing SystemVerilog assertions.
Why Do We Need Assertions?
An assertion is nothing but a more concise representation of a functional checker. The same functionality can also be written as a SystemVerilog task or checker involving more lines of code, but this has real disadvantages:
- SystemVerilog is verbose, and it's difficult to maintain and scale code as the number of properties grows
- Being a procedural language, it's difficult to write checkers that involve many parallel events happening in the same period of time
// A property written in Verilog/SystemVerilog
always @ (posedge clk) begin
if (!(a && b))
$display ("Assertion failed");
end
SystemVerilog Assertions is a declarative language used to specify temporal conditions, and is far more concise and easier to maintain:
// The property above written in SystemVerilog Assertions syntax
assert property(@(posedge clk) a && b);
Quick Check
Q: Beyond just being shorter, why is the SVA version considered more maintainable as a project grows?
Show Answer
SVA properties are independent, composable units, declared separately from the procedural flow of the testbench. Procedural checker code tends to become tangled as more properties are added, since each one has to be manually threaded into the existing control flow — SVA properties don't have that problem.
Types of Assertion Statements
| Type | Description |
|---|---|
| assert | Specifies that the given property of the design is true in simulation |
| assume | Specifies that the given property is an assumption, used by formal tools to generate input stimulus |
| cover | Evaluates the property for functional coverage |
| restrict | Specifies the property as a constraint on formal verification computations, and is ignored by simulators |
This chapter focuses on assert and cover, since they're the two most directly relevant to simulation-based verification. assume and restrict matter primarily to formal verification tools — see Assertion Coverage on the Verification tutorial for how all four are actually used together in a real coverage-driven flow.
Building Blocks of Assertions
Sequence
A sequence of multiple logical events typically forms the functionality of any design. These events may span across multiple clocks or exist for just a single clock cycle. To keep things simple, smaller events can be represented using simple assertions, which can then be used to build more complex behavior patterns:
// Sequence syntax
sequence
endsequence
// Assert the sequence
assert property ();
Property
These events can be represented as a sequence, and a number of sequences can be combined to create more complex sequences or properties. It's necessary to include a clocking event inside a sequence or property in order to assert it:
// Property syntax
property
or
endproperty
// Assert the property
assert property ();
There are two kinds of assertions: immediate and concurrent.
Immediate Assertions
Immediate assertions are executed like a statement in a procedural block and follow simulation event semantics. They're used to verify an immediate property at the exact point in the code they appear:
always @ () begin
...
// This is an immediate assertion executed only
// at this point in the execution flow
$assert(!fifo_empty); // Assert that fifo is not empty at this point
...
end
See SystemVerilog Immediate Assertions for the full depth on these, including how they behave in both design and testbench code.
Concurrent Assertions
Concurrent assertions are based on clock semantics and use sampled values of their expressions. Circuit behavior is described using SystemVerilog properties that get evaluated every time on the given clock, and a failure in simulation indicates the described functional behavior was violated:
// Define a property to specify that an ack should be
// returned for every grant within 1:4 clocks
property p_ack;
@(posedge clk) gnt ##[1:4] ack;
endproperty
assert property(p_ack); // Assert the given property is true always
See SystemVerilog Concurrent Assertions for the full depth on these, including exactly when sampled values are captured relative to the clock edge.
Steps to Create an Assertion
- Create boolean expressions
- Create sequence expressions
- Create a property
- Assert the property
A Complete Example
The first sequence s_ab validates that b is high the next clock when a is high, and the second sequence s_cd validates that d is high 2 clocks after c is found high. The property asserts that the second sequence starts exactly one cycle after the first sequence completes:
module tb;
bit a, b, c, d;
bit clk;
always #10 clk = ~clk;
// This is just a stimulus to trigger assertions
initial begin
for (int i = 0; i < 20; i++) begin
{a, b, c, d} = $random;
$display("%0t a=%0d b=%0d c=%0d d=%0d", $time, a, b, c, d);
@(posedge clk);
end
#10 $finish;
end
// Step 2. Create sequence (optional), else add
// boolean expr directly inside a property
sequence s_ab;
// Step 1. Create a boolean expression
a ##1 b;
endsequence
// Step 2. Create sequence (optional)
sequence s_cd;
// Step 1. Create a boolean expression
c ##2 d;
endsequence
// Step 3. Create property
property p_expr;
@(posedge clk) s_ab ##1 s_cd;
endproperty
// Step 4. Assert property
assert property (p_expr);
endmodule
Note that there are some violations for the property that is asserted using the assert statement.
Output
Compiler version P-2019.06-1; Runtime version P-2019.06-1; Jan 8 05:02 2020
Warning : License for product VCSRuntime_Net(725) will expire within 10 days, on: 17-jan-2020.
If you would like to temporarily disable this message, set
the VCS_LIC_EXPIRE_WARNING environment variable to the number of days
before expiration that you want this message to start (the minimum is 0).
0 a=0 b=1 c=0 d=0
10 a=0 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 10ns failed at 10ns
Offending 'a'
30 a=1 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 30ns failed at 30ns
Offending 'a'
50 a=0 b=0 c=1 d=1
70 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 70ns failed at 70ns
Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 50ns failed at 70ns
Offending 'b'
90 a=1 b=1 c=0 d=1
110 a=0 b=1 c=0 d=1
130 a=0 b=0 c=1 d=0
"testbench.sv", 28: tb.unnamed$$_3: started at 130ns failed at 130ns
Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 90ns failed at 130ns
Offending 'c'
150 a=0 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 150ns failed at 150ns
Offending 'a'
170 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 170ns failed at 170ns
Offending 'a'
190 a=0 b=1 c=1 d=0
210 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 210ns failed at 210ns
Offending 'a'
230 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 190ns failed at 230ns
Offending 'c'
250 a=1 b=1 c=0 d=0
270 a=1 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 230ns failed at 270ns
Offending 'c'
290 a=0 b=1 c=1 d=0
"testbench.sv", 28: tb.unnamed$$_3: started at 270ns failed at 290ns
Offending 'b'
"testbench.sv", 28: tb.unnamed$$_3: started at 250ns failed at 290ns
Offending 'c'
310 a=0 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 310ns failed at 310ns
Offending 'a'
330 a=1 b=0 c=1 d=0
"testbench.sv", 28: tb.unnamed$$_3: started at 330ns failed at 330ns
Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 290ns failed at 330ns
Offending 'c'
350 a=0 b=1 c=0 d=1
370 a=0 b=1 c=1 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 370ns failed at 370ns
Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 390ns failed at 390ns
Offending 'a'
$finish called from file "testbench.sv", line 13.
$finish at simulation time 400
V C S S i m u l a t i o n R e p o r t
Notice how many separate assertion attempts are running at once — a new attempt at s_ab starts on every clock edge, so several overlapping instances are always in flight, each independently tracked until it passes, fails, or is superseded. The "Offending" line tells you exactly which part of the composed sequence broke: 'a' means s_ab itself never got started correctly; 'b' means s_ab started but its own second half failed; 'c' means s_ab completed fine but s_cd's own first half then failed.
Quick Check
Q: If s_ab completes successfully at some cycle N, at which cycle does the property expect s_cd to begin?
Show Answer
Cycle N+1. The property's own ##1 between s_ab and s_cd requires s_cd to start exactly one clock cycle after s_ab finishes — not on the same cycle, and not any later than that.
Where Is This Used?
A realistic request-grant-data handshake — a request is followed by a grant within a bounded window, and the grant is followed by valid data some fixed number of cycles later — is exactly the kind of multi-part protocol behavior this chained-sequence pattern is built for. Real verification IP typically has dozens of properties like this bundled together, checking every stage of a protocol handshake simultaneously.
Common Beginner Mistakes
Mistake #1: Writing procedural checker code when a declarative property would be simpler
As the "Why Do We Need Assertions?" section shows, a single line of SVA can replace several lines of procedural always-block logic. Why? Procedural checkers get harder to maintain as more rules are added; a declarative property stays a self-contained, independent statement no matter how many others exist alongside it.
Mistake #2: Confusing assert with assume
assert checks that a property holds; assume tells a formal tool to treat a property as a given constraint on its input generation. Why? These serve fundamentally different roles — using assume where you meant assert means you're no longer actually checking that property at all in a formal context.
Mistake #3: Expecting restrict to do anything in simulation
restrict is explicitly ignored by simulators. Why? It only has meaning to formal verification tools, as a constraint on the state space they explore — writing one and expecting a simulation-time check is a fundamental misunderstanding of what it's for.
Mistake #4: Forgetting a sequence or property needs a clocking event
A sequence or property needs a clocking event specified before it can be meaningfully asserted. Why? Without one, there's no defined point in time at which the expression is actually sampled and evaluated — concurrent assertions are fundamentally clock-driven.
Practice Exercise
Challenge: Build a Two-Sequence Property
Write a property that checks: whenever req is high, busy must be high on the very next clock, and done must be high exactly 3 clocks after that. Structure it as two named sequences combined with ##1, the same pattern as s_ab/s_cd in this article.
Hint
The first sequence checks req followed by busy one cycle later; the second checks a starting condition followed by done three cycles later. Combine them exactly the way p_expr combines s_ab and s_cd.
Solution
sequence s_req_busy;
req ##1 busy;
endsequence
sequence s_start_done;
busy ##3 done;
endsequence
property p_handshake;
@(posedge clk) s_req_busy ##1 s_start_done;
endproperty
assert property (p_handshake);
This checks the full handshake in one property: req triggers busy one cycle later, and starting one cycle after that, the same busy condition must hold, followed by done three cycles after it — exactly the same chained-sequence structure as the article's own s_ab/s_cd example, applied to a realistic handshake instead of arbitrary boolean signals.
Summary
In this tutorial, you learned:
- A property describes something a design must always do, or must never do — an assertion fails when either kind of property is violated
- SVA is declarative, making it far more concise and maintainable than writing equivalent checker logic procedurally
- The four assertion statement types are
assert,assume,cover, andrestrict— each with a distinct role, and onlyassert/covermattering directly to simulation - A
sequencedescribes a boolean or temporal expression; apropertycombines sequences into more complex checks, and both require a clocking event before they can be asserted - Multiple sequences can be chained together with
##to build up a multi-stage protocol check from smaller, independently-named pieces
