Hi All,
I have a doubt in below assertion execution
property p_1
@(posedge clk) a |=> b[=2] ##1 c ;
endproperty : p_1
So If suppose my sampled values are like this assertion will pass
run -all
#0 clk=1, a=0, b=0, c=0
#5 clk=1, a=1, b=0, c=0 // a got asserted (antecedent got triggered)
#10 clk=1, a=0, b=0, c=0
#15 clk=1, a=0, b=1, c=0 // 1st b=1
#20 clk=1, a=0, b=0, c=0
#25 clk=1, a=0, b=1, c=0 // 2nd b=1
#30 clk=1, a=0, b=0, c=0
#35 clk=1, a=0, b=0, c=1 // Property Passed
and If my sampled values are like below will my assertion pass ?
run -all
#0 clk=1, a=0, b=0, c=0
#5 clk=1, a=1, b=0, c=0 // a got asserted (antecedent got triggered)
#10 clk=1, a=0, b=0, c=0
#15 clk=1, a=0, b=1, c=0 // 1st b=1
#20 clk=1, a=0, b=0, c=0
#25 clk=1, a=0, b=1, c=0 // 2nd b=1
#30 clk=1, a=0, b=0, c=0
#35 clk=1, a=0, b=1, c=1 // Property Passed or Fail ?
So at #35 time unit b and c are 1 and also b is 1 for 3 times
but as per our property b=1 appeared 2 times and after 1 clock cycle delay c=1 is happening. So , here will our simulation consider b also ?
Thanks You