|
|
|
|
|
|
|
|
|
|
|
|
Concurrent assertions
|
|
|
Concurrent assertions describe behavior that spans over time. Concurrent assertion is evaluated only at the occurrence of a clock tick. The values of variables used in the evaluation are the sampled values. This way, a predictable result can be obtained from the evaluation, regardless of the simulator's internal mechanism of ordering events and evaluating events. This model of execution also corresponds to the synthesis model of hardware interpretation from an RTL description. |
|
|
|
|
|
An expression used in an assertion is always tied to a clock definition. The sampled values are used to evaluate value change expressions or boolean subexpressions that are required to determine a match of a sequence. The keyword property distinguishes a concurrent assertion from an immediate assertion. |
|
|
|
|
|
|
|
|
Below is image showing when a signal is sampled with respect to clock and simulation ticks. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Concurrent assertions have following layers. |
|
|
|
|
|
- Boolean
- Sequences
- Property
- Property directive
|
|
|
|
|
|
Before we look at each of these layer in detail, lets look at a simple example first which tests below waveform |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Example : Concurrent Assertion
|
|
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module concurrent_assertion(
5 input wire clk,req,reset,
6 output reg gnt);
7 //=================================================
8 // Sequence Layer
9 //=================================================
10 sequence req_gnt_seq;
11 // (~req & gnt) and (~req & ~gnt) is Boolean Layer
12 (~req & gnt) ##1 (~req & ~gnt);
13 endsequence
14 //=================================================
15 // Property Specification Layer
16 //=================================================
17 property req_gnt_prop;
18 @ (posedge clk)
19 disable iff (reset)
20 req |-> req_gnt_seq;
21 endproperty
22 //=================================================
23 // Assertion Directive Layer
24 //=================================================
25 req_gnt_assert : assert property (req_gnt_prop)
26 else
27 $display("@%0dns Assertion Failed", $time);
28 //=================================================
29 // Actual DUT RTL
30 //=================================================
31 always @ (posedge clk)
32 gnt <= req;
33
34 endmodule
35
36 //+++++++++++++++++++++++++++++++++++++++++++++++
37 // Testbench Code
38 //+++++++++++++++++++++++++++++++++++++++++++++++
39 module concurrent_assertion_tb();
40
41 reg clk = 0;
42 reg reset, req = 0;
43 wire gnt;
44
45 always #3 clk ++;
46
47 initial begin
48 reset <= 1;
49 #20 reset <= 0;
50 // Make the assertion pass
51 #100 @ (posedge clk) req <= 1;
52 @ (posedge clk) req <= 0;
53 // Make the assertion fail
54 #100 @ (posedge clk) req <= 1;
55 repeat (5) @ (posedge clk);
56 req <= 0;
57 #10 $finish;
58 end
59
60 concurrent_assertion dut (clk,req,reset,gnt);
61
62 endmodule
You could download file concurrent_assertion.sv here
|
|
|
|
|
|
In the above code, all the layers of Concurrent assertions are shown. The basic building blocks are boolean layer, which evalutes to TRUE or FALSE. Sequence is basically built on top of boolean layer. A sequence is the most basic construct for defining any concurrent assertion. Property layer is build on top of sequence layer (Not always). To make a property to be part of a simulation it needs to be used in assert statement. Which basically tells the simulator to test the property for correctness. |
|
|
|
|
|
Now that we have looked at the basic flow of assertion in SystemVerilog, lets look at each of the layers in detail. |
|
|
|
|
|
Simulation : Concurrent Assertion
|
|
|
|
|
|
@129ns Assertion Failed
@237ns Assertion Failed
@243ns Assertion Failed
@249ns Assertion Failed
@255ns Assertion Failed
@261ns Assertion Failed
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Copyright © 1998-2014 |
Deepak Kumar Tala - All rights reserved |
Do you have any Comment? mail me at:deepak@asic-world.com
|
|