|
|
|
|
|
|
|
|
|
|
|
Introduction
|
|
|
Verification with assertions refers to the use of an assertion language to specify expected behavior in a design, Tools that evaluate the assertions relative to the design under verification |
|
|
|
|
|
Assertion-based verification is of most use to design and verification engineers who are responsible for the RTL design of digital blocks and systems. ABV lets design engineers capture verification information during design. It also enables internal state, datapath, and error precondition coverage analysis. |
|
|
|
|
|
Simple example of assertion could be a FIFO, when ever ever FIFO is full and write happens, it is illegal. So designer of FIFO can write assertion which checks for this condition and asserts failure. |
|
|
|
|
|
Most assertions can be written in HDL, but HDL assertions can be lengthy and complicated. This defeats the purpose of assertions, which is to ensure the correctness of the design. Lengthy, complex HDL assertions can be hard to create and subject to bugs themselves. |
|
|
|
|
|
SystemVerilog has features to specify assertions of a system. An assertion specifies a behavior of the system. Basically SVA or SystemVerilog Assertions is based on PSL assertions, that was developed earlier. |
|
|
|
|
|
SystemVerilog Assertions can be classified into two types |
|
|
|
|
|
- Immediate Assertions : Follow simulation event semantics, like code in always block.
- Concurrent Assertions : Based on clock semantics, like always block with clock.
|
|
|
|
|
|
We will see both of them in detail in next few pages. |
|
|
|
|
|
|
|
|
|
|
|
Immediate Assertions
|
|
|
The immediate assertion statement is a test of an expression performed when the statement is executed in the procedural code. If the expression evaluates to X, Z or 0, then it is interpreted as being false and the assertion is said to fail. Otherwise, the expression is interpreted as being true and the assertion is said to pass. Immediate assertions are roughly equivalent of VHDL assert statement. |
|
|
|
|
|
assertion_label : assert (expression)
pass block code;
else
fail block code;
|
|
|
|
|
|
Where : |
|
|
|
|
|
- assertion_label : User defined assertion label.
- assert : SystemVerilog reserve word, used for assertion.
- expression : Any valid verilog expression.
- pass block code : Code that gets executed when assertion passes.
- else : Optional syntax to specify failed code.
- fail block code : Code that gets executed when assertion fails.
|
|
|
|
|
|
Normally we prefer to print some message for pass or fail block code. SystemVerilog provides various assertions levels for reporting messages as listed below. |
|
|
|
|
|
- $fatal is a run-time fatal.
- $error is a run-time error.
- $warning is a run-time warning, which can be suppressed in a tool-specific manner.
- $info indicates that the assertion failure carries no specific severity.
|
|
|
|
|
|
One can use $display, or any regular verilog code, like triggering a event, or incrementing a counter, or calling function in pass/fail block code. |
|
|
|
|
|
Example - Assert Immediate
|
|
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With Immediate assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module assert_immediate();
5
6 reg clk, grant, request;
7 time current_time;
8
9 initial begin
10 clk = 0;
11 grant = 0;
12 request = 0;
13 #4 request = 1;
14 #4 grant = 1;
15 #4 request = 0;
16 #4 $finish;
17 end
18
19 always #1 clk = ~clk;
20 //=================================================
21 // Assertion used in always block
22 //=================================================
23 always @ (posedge clk)
24 begin
25 if (grant == 1) begin
26 CHECK_REQ_WHEN_GNT : assert (grant && request) begin
27 $display ("Seems to be working as expected");
28 end else begin
29 current_time = $time;
30 #1 $error("assert failed at time %0t", current_time);
31 end
32 end
33 end
34
35 endmodule
You could download file assert_immediate.sv here
|
|
|
|
|
|
Simulator Output - Assert Immediate
|
|
|
|
|
|
Info: "assert_immediate.sv", 21:
assert_immediate.CHECK_REQ_WHEN_GNT: at time 9
Seems to be working as expected
Info: "assert_immediate.sv", 21:
assert_immediate.CHECK_REQ_WHEN_GNT: at time 11
Seems to be working as expected
"assert_immediate.sv", 21:
assert_immediate.CHECK_REQ_WHEN_GNT:
started at 13s failed at 13s
Offending '(grant && request)'
Error: "assert_immediate.sv", 21:
assert_immediate.CHECK_REQ_WHEN_GNT: at time 14
assert failed at time 13
"assert_immediate.sv", 21:
assert_immediate.CHECK_REQ_WHEN_GNT:
started at 15s failed at 15s
Offending '(grant && request)'
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|