Assertion Question

Hi,

Kindly help on this Assertion Question
we want RESET should be high for the first 3 clock ticks of our simulation and then it should predominantly stay zero.

In reply to Rohith V:

Not sure what you mean by “predominantly”, but if you mean never high again:

initial assert property ( @(posedge clk)
                     rst[*3] #=# always !rst
                    );

Hello,
what does this mean in the above assertion property, #=#
Please assist.

In reply to ronankilakshmi:

IEEE 1800-2009 provided the capability of defining a property that follows a sequence by zero or one cycle delay, starting from the end point of the sequence. This capability is introduced with the followed-by operators #-# and #=# that concatenate a sequence and a property. The followed-by operators are of the following forms for the definition of a property:
[1] sequence_expr #-# property_expr // concatenation with zero cycle delay
| sequence_expr #=# property_expr // concatenation with one cycle delay

The equivalence of sequence_expr #-# property_expr is defined as:
not (sequence_expr |-> not property_expr)
and the equivalence of sequence_expr #=# property_expr is:
not (sequence_expr |=> not property_expr)

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

Thank you for the response.

In SVA, can we also use ## for one clock cycle delay. Please assist.