Hi all,
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?
Thank you.
