When to use implication and when to use ##delay in system verilog assertions

SystemVerilog
1

I have scenario of SV assertion where first a should be high 1 cycle after this b should be high and 1 cycle after that c should be high, after this with 1 cycle delay d should be high I am confused as to how this assertions should be coded. I have three options please help me which should be followed as correct solution

Option1 : a |=> b |=> c |=> d ;

Option2 : a |=> b ##1 c ##1 d;

Option3 : a ##1 b |=> c ##1 d;

Option4 : a ##1 b ##1 c ##1 d;

I am getting stuck at these options which one to follow . Please guide me about best solution and as to why

2

In reply to munish37:
The key difference how you want to define pass or failure in an assertion . ##1 is a sequence operator; |=> is a property operator. The result of a sequence is a pattern match, and the result of a property is true or false. A sequence by itself can be asserted as a property, which means every clock cycle it attempts to find a match. Each attempt that it doesn’t find a match is a failure.

Let’s take the sequence
a ##1 b;. This says look for a match when a is high followed in the next clock cycle when b is high. But as an asserted property

assert property (a ##1 b);

This fails every clock cycle a is not true, as well as every clock cycle a is true followed by b not true.
If you only care that b is true a clock cycle after a is true, that’s when you use the implication.

assert property (a |=> b);

If a is false, the property passes, otherwise if a is true, b must be true the next cycle.

3

In reply to dave_59:

Thanks dave_59 for your reply and clarifying that It is upto the user how user want to define pass or failure in an assertion