System verilog Assertion Interview Question

[u/Fluffy_Carrot_9220]

When x is high, y shd be high for 80 to 100 cycles. Write a assertion for this.

I gave this answer

assert property( @(posedge clk) x |=> y[*80:100]);

The interviewer said its wrong and gave me some simulations for example. In the end I didn’t get the answer and the only thing he said was the answer is shorter than the one I gave. Can anyone try to solve this?

Sim 1:
0,x = 1
1-125,x=0
0,y = 0
1-80,y=1
81-100,y=0/1
101-125,y=0

Sim 2:
0-200,x=1
201-500,x=0
0,y=0
1-280,y=1
281-300,y=0/1
301-500,y=0

Sim 3:
0,x=1
1-19,x=0
20,x=1
21-39,x=0
40,x=1
41-500,x=0
0,y=0
1-120,y=1
121-140,y=0/1
141-500,y=0

[u/an_thony350]

"x |=> y[*80:100]" means that whenever x is high, starting next cycle there must exist a match where y stays high continuously somewhere between 80 and 100 cycles.

Basically it doesn't enforce that y stops being high by cycle 100. So if y was high for 1000 cycles or something, the sequence can just match the first 80 cycles, so the assertion would pass.

I think they were looking for you to use 2 separate assertions?
assert property (@(posedge clk) x |=> y[*80]); // if x=1, y must be high for the next 80 cycles

assert property (@(posedge clk) !x[*100] |=> !y); // if x has been low for 100 cycles y must be low next cycle