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.
