SVA
SystemVerilog Assertions: A Comprehensive Guide
In the world of hardware design, simply creating a circuit isn't enough. You also have to prove that it works exactly as intended. One of the most powerful ways to do this is through formal verification, and a key component of that is using SystemVerilog Assertions (SVAs).
SVAs are properties, or statements, that define the expected behavior of your design. They act as a formal specification, allowing tools to mathematically check for correctness. The industry standard for these properties is defined by IEEE 1800-2017.
The Three Basic Types of SVA Statements
There are three fundamental types of statements you can use in SVA to define the correctness of your design:
- Assertions: These are statements about your design's behavior that should always be true. For example, you might assert that a bus protocol's handshake signals never go high at the same time.
- Assumptions: These statements define constraints on the verification environment. They describe the behavior of the "world" outside of your design, which helps the formal tool understand the conditions under which your design operates.
- Cover Properties: These are used to describe interesting or critical behaviors that should be reached during verification. They're a way to ensure that you've tested specific scenarios in your design.
Immediate vs. Concurrent Assertions
When you're writing assertions, you'll encounter two main types:
- Immediate Assertions: These are the simplest kind of assertion. They don't rely on clocks or resets and are evaluated immediately when their procedural code is executed. Think of them like a simple
ifstatement that checks for a condition right now. - Concurrent Assertions: These are the most suitable for verifying complex behavior that unfolds over time. They support clocks and resets, making them ideal for checking signal sequences, timing relationships, and other intricate features that are typical in modern hardware designs. For formal property verification (FPV), concurrent assertions are highly recommended over immediate ones.
Best Practices for Writing Assertions
SVA Syntax: A Layered Approach
SystemVerilog Assertions (SVA) can be understood as a series of building blocks, starting with the simplest expressions and building up to complex properties. Think of it as a pyramid with four distinct layers:
- Booleans: At the very foundation are simple Boolean expressions. These are combinatorial expressions that evaluate to
trueorfalseat a single moment in time. They are the atomic units of an SVA. - Sequences: The next layer is made of sequences. A sequence is a finite list of Boolean expressions evaluated in a specific, linear order over multiple clock cycles. A sequence tries to match a particular pattern of Boolean expressions over time. For example, a sequence could define that signal
Amust be high one cycle after signalBgoes low. - Properties: Building upon sequences are properties. A property is a collection of sequences that defines when to start and end the sequence or sequences. It also defines the conditions under which a sequence is considered to have passed or failed.
- Assertion Directives: The final, top layer is the assertion directive. This is what actually creates an instantiation of a property and tells the verification tool what action to take if the property passes or fails. The directives are the
assert,assume, andcoverstatements we've previously discussed.
Key Sequence Operators
These operators let you define specific timing relationships and repetitions within a sequence.
|->: The Overlapped Implication operator. Checks if the second sequence holds true starting in the same clock cycle as the first.|=>: The Non-overlapped Implication operator. Checks if the second sequence holds true starting in the next clock cycle after the first.##n: A Fixed Delay ofnclock cycles.##[a:b]: A Variable Delay betweenaandbcycles.[*]n: A Fixed Consecutive Repetition ofncycles.[*][a:b]: A Variable Consecutive Repetition ofatobcycles.
Auxiliary Code & System Functions
Formal verification often involves intricate behavior that's tough to capture in a single property. That's where auxiliary code comes in. This is regular SystemVerilog code, like a counter or a state machine, that helps you keep track of complex states or behaviors. You can then write a simple assertion on the value of a variable in that auxiliary code. This makes your properties much easier to read and debug.
Sampled Value Functions
These functions allow you to access past values of signals, which is critical for defining temporal behavior.
$past(expr, n): Returns the value ofexprncycles earlier.$rose(expr): Checks if the expression value rose (changed from 0 to 1) in the previous cycle.$fell(expr): Checks if the expression value fell (changed from 1 to 0) in the previous cycle.$changed(expr): Checks if the expression value changed from the previous cycle.$stable(expr): Checks if the expression value remained stable from the previous cycle.
Best Practices & Advanced Features
- Handle Abort Conditions: Use the
disable iffclause to temporarily suspend an assertion, for example, during a reset. - Liveness Properties: These deal with the question, "Will something good always eventually happen?" The
s_eventuallyoperator is particularly useful for this. - Verification Directives: A property declaration is just a definition. You must use a directive like
assert,assume, orcoverto tell the formal tool to actually check the behavior.
Example: Using Auxiliary Code
Here is an example demonstrating the use of auxiliary code to track a counter and assert its maximum value.
bit [3:0] aux_counter;
always @(posedge clk) begin
if (rst) begin
aux_counter <= 0;
end else begin
if (dut.output_valid) begin
aux_counter <= aux_counter + 1;
end
end
end
P1: assert property (
@(posedge clk) disable iff (rst)
aux_counter < 8
);
Comments