SystemVerilog Assertion (SVA) Implication with Preemtive Start

Question

I'm a newbie in SVA. I have a question about the SVA implication.

1: sequence s1;
2:   start ##[1:$] !start;
3: endsequence: s1
4:
5: sequence s2;
6:   ready && (!start);
7: endsequence: s2;
8: 
9: assert_ready: assert property (@(posedge clk) s1 |-> ##5 s2);

The purpose of this assertion is to check the timing property:

• when 'start' is toggled, 'ready' is activated after 5 clock cycle.
• But, when there is a preemtive 'start', that is, another 'start' toggle before 'ready' is activated, this timing property should be reset and the 'ready' should be muted.

I tried to verify this property by using the formal verification tool, Synopsys' VC formal. What it shows that this assertion fails because s2 sequence is zero when preemtive 'start' happens.

I think I have a wrong description at line 6, which is a real newbie code. Would you please let me know how to describe the assertion for the preemtive start correctly?

Answer 1

I think you want

sequence s1;
   start ##1 !start [*5]
endsequence: s1
sequence s2;
  ready;
endsequence: s2;

assert_ready: assert property (@(posedge clk) s1 |->  s2);

Although you might have to adjust this depending on your requirement on what happens when start coincides with ready on the 5th cycle.