Hi,
I am trying to write following property. As per my understanding of ‘or’ construct if sig is deasserted or if $time-t3 becomes > 100ns antecedent should become true. But I see that even though sig is deasserted much before consequent is evaluated only when $time-t3>100ns. What is wrong with following property.
property test1;
time t3,t4;
@(posedge clk)disable iff(reset==1)($rose(sig),t3=$time) ##1((!sig[->1]) or (($time-t3)>100ns)[->1]) |-> !sig;
endproperty:test1
// You need a first_match because you have multiple threads,
// and all threads of an antecedent must be tested before the assertion terminates.
// Thus, if sig==1'b1 before ($time-t3)>100ns), the assertion will terminate when
// ($time-t3)>100ns) is true. Thus, change the property to:
//--------------------------------------------------------------------------
property test1;
time t3,t4;
@(posedge clk)disable iff(reset==1)
first_match(
(($rose(sig),t3=$time) ##1 !sig[->1]) or (($time-t3)>100ns)[->1]
) |-> !sig;
endproperty:test1