In reply to Vignesh Raghavan:
As I understand, Since at every sampling clock, the local variable v to the property is created newly and used for asserting if the property holds, hence, v will be initialised to 0 when bit[16:0] v; statement is executed. By default, SV assigns ‘0’ to 2-state variables (here, bit[16:0] v).
Is that the reason behind why we can ignore v=0 in the property expression?
The short answer is YES.
The formal answer is from 1800, specifically,
16.8.2 Local variable formal arguments in sequence declarations
In general, a local variable formal argument behaves in the same way as a local variable declared in an
assertion_variable_declaration. The rules in 16.10 for assigning to and referencing local variables,
including the rules of local variable flow, apply to local variable formal arguments with the following
provisions:
Without further specification, the term local variable shall mean either a local variable formal
argument or a local variable declared in an assertion_variable_declaration.
— At the beginning of each evaluation attempt of an instance of a named sequence, a new copy of each
of its local variable formal arguments shall be created.
Ben Cohen
SystemVerilog.us