I am reading SVA: The Power of Assertions in SystemVerilog.
At page 102,
Example 5.5. For a Boolean expression e , always e is true iff e is true in every clock tick.
Example 5.6. What is the meaning of nexttime always p ?
Solution: According to the definition of nexttime property, always p should hold
in clock tick 1. Therefore, property p should hold in every clock tick starting from
clock tick 1.
Here in Ex 5.5 ‘e’ is considered as boolean expression and in Ex 5.6 p is considered as boolean property. why?
Also i didn’t fully understood the need of always operator.
initial assert property(@(posedge clk) always a);
only checks at first posedge clk. Then writing always property to ‘a’ redundant?
assert property(@(posedge clk) always a);
will check a at every posedge clk. i.e an implicit always is present. here also writing always to ‘a’ is redundant. one can write simply ‘a’ am i right?
// 1800'2017 syntax defines a property as one of the following
property_expr ::=
sequence_expr
| ( property_expr )
| ... // see 1800
| sequence_expr #-# property_expr
| sequence_expr #=# property_expr
| nexttime property_expr
| nexttime [ constant _expression ] property_expr
| s_nexttime property_expr
| s_nexttime [ constant_expression ] property_expr
| always property_expr
| always [ cycle_delay_const_range_expression ] property_expr
| s_always [ constant_range] property_expr
| ... // see 1800
property p;
nexttime [k] property_expr; // k is a constant_expression
endproperty
// Is equivalent to
property p_eqiv;
##k 1'b1 #-# property_expression);
endproperty
// 'e' is considered as boolean expression and in Ex 5.6 p is considered as boolean property.
a |-> always e; // e is a sequence of 1 term that is interpreted as a property
// The always requires a property
// The syntax option for a property is a sequence
a |-> nexttime always p; // nextime (property_expr)
// always(property_expr)
// nexttime property, always p should hold
// in clock tick 1.
// Therefore, property p should hold in every clock tick starting from
// [Ben] the next clock tick
// Thus,
nexttime always p; // same as the property
##1 1'b1 #_# always(p); // p is a property or a sequence interpreted as a property
// A boolean is a sequence of length ONE.