Now a days Assertion Based Verification (ABV) is getting important place in the verification flows with lots of organizations. So its obvious to have the curiosity to understand about ABV. But first we need to understand, “What is an Assertion?”
“Assertion is a statement that a certain design property must be true”
An assertion is failed during simulation in following two conditions:
- If the design property does not behave the way we expect it to.
- If the design property is forbidden from happening.
Assertions can be used very effectively as a debugging technique in the design verification process.
While developing the assertions for a design, the functional specification document of the design work as an input source & infer a list of properties by converting (coded) these properties into SystemVerilog Assertions (SVA). These assertions are continuously monitored during simulation life time. Not only this, same set of assertions can be used during formal verification. Though the monitors/checkers can be written using Verilog language but formal verification support is not possible for the monitor code written in the procedural verilog code.
Verilog have certain limitation as far as monitors/checkers implementation is concerned, these limitations are as follows:
- Verilog being a procedural language does not have very good control over time.
- Verilog is a verbose language hence it require large piece of code for the same assertion. In addition, in case of large number of assertions, its difficult to maintain the code.
- Procedural nature of Verilog language makes it hard to test the parallel events in the same time period. Sometime Verilog might miss the triggered events as well.
- Verilog does not provide any built-in mechanism for generating functional coverage metrics.
SVA is a concise language, which compress the required code for the same assertion and is handy to maintain the code for large number of assertions. SVA being the declarative language provides a great control over time & very good for temporal conditions (sequence of events in the time domain). SVA provides built-in functions to test certain design conditions & provides mechanism to generate functional coverage automatically.
Lets see an example of a monitor code implemented in Verilog and SVA:
Following monitor/checker code is written to capture the condition that after the signal “req” is asserted, signal “ack” must be asserted with-in 1 to 3 clock cycles.
Verilog code:
module ack_after_req();
reg req, ack, clk;
initial begin
req = 0;
ack = 0;
clk = 0;
#10 req = 1;
#45 ack = 1;
#25 $finish;
end
always
#5 clk = !clk;
////////////// Verilog Checker Start ///////////
always@(posedge req)
begin
repeat(1)@(posedge clk);
fork: ack_after_req
begin
@ (posedge ack)
$display(“ack appreared with-in 1-3 clocks after req”);
disable ack_after_req;
end
begin
repeat(3)@(posedge clk);
$display(“ack DID NOT appeared with-in 1-3 clocks after req”);
disable ack_after_req;
end
join
end
///////////////// Verilog Checker End //////////////
endmodule
SystemVerilog Assertion (SVA) Code:
/////////////// SVA Start /////////////////
ack_after_req:
assert property
(@(posedge clk) $rose(req) |-> ##[1:3] $rose(ack));
////////////// SVA End ////////////////////
Further Assertion Topics:
Following listed various concepts are associated with the Assertions. Some of these concepts are related to each other as shown in the diagram below. I’ll write down about more of these concepts in my upcoming posts. By then, these are here for introduction/reference and further exploration by you.
- Immediate Assertions
- Concurrent Assertions
- Implication
- Properties
- Sequences
- Properties & Sequence Variables
- Clubbing Sequences
- Assertion Clocking
- Binding
- System Functions
- Assertion Coverage
I hope this post would be able to provide a brief introduction about “SystemVerilog Assertions” and contrast with Verilog language. I’ll post on further Assertion topics soon.
Thank you for your time to go through this post!
Hi,
Thanks for the post (Basics about Assertions..??).
Where can i find the continuation of these topics?
Thanks
Haniel