Lets look at the basic syntax of a system verilog assertion.
Assertion_Label: assert property (@(<clocking>) <filter> <expression> );
The above syntax represented in a example is as follows.
req_grant_check: assert property (@(posedge clk) disable iff (rst_n) ($rose(req |=> ##[1:3] gnt));
Splitting the example into language fields:
Assertion_Label: req_grant_check
clocking : posedge clk
filter : disable iff (!rst_n)
expression : ($rose(req |=> ##[1:3] gnt)
The assertion label is used to differentiate the different assertions.
Clocking is the clock or trigger on which the assertion should be evaluated. The assertion is triggered and evaluated on this.
Filter is the condition on which the checking can be skipped. In this case we are skipping when the reset is asserted and checking is enabled only when out of reset, Any boolean expression can be used as filter. Please note ‘iff’ is the syntax for filtering, and is not ‘if’.
Expression is the actual check that has be executed. In this case we are checking that grant should be asserted within three clocks of assertion of request.
Assertion
An assertion is a property description. This property is being continuously evaluated in the course of simulation and if the property is not satisfied at any instant of time the assertion fails. Assertions are not a new feature and can be viewed as a monitor or checker that used to be written in Verilog using procedural code. Assertion based languages and PSL (Property Specification Language) SVA (System Verilog Assertions) provide better language constructs developed specifically for property checking. These eliminate some of the difficulties encountered when using a procedural code like verilog.
SVA is declartive code and meant specifically for property checking. Lets look at an example temporal check.
e.g. 1. Arbiter
The request to the arbiter is asserted on the posedge of the clock. The grant should be asserted within a maximum of 60 clocks. If the particular device doesnt get a grant within 50 clocks then the arbiter logic fails.
req_grant_checker_devA:
assert propery (@(posedge clk) $rose(req) | -> ##[1:50] $rose(grant));
The same checker written in procedural verilog could have ended up very verbose.
Having learnt what is the advantage of assertion based verification, lets get into details of the language in future tutorials. Happy Blogging.
