Hi All,
Generally, the clocking event of concurrent assertion is actually a clock signal
property sva1;
@(posedge clk) <property_expression1>;
endproperty
In rare cases where I want to check for FSM state transition one could use ps_state as the clocking event which would trigger sva2 only when state changes.
property sva2;
@(ps_state) <property_expression2>;
endproperty
From LRM perspective the above code is perfectly legal
On comparing the above two properties my understanding is that using @(posedge clk) the property would execute numerous times in a simulation even when there is no transition in ps_state.
Such unnecessary attempts are avoided in sva2 which I feel could be possibly better from a tool perspective
I was specifically looking to hear from people with hands-on experience using formal tools whether the sva2 is legal in a formal testbench ?
Are there any disadvantages with using ps_state as a clocking event of a concurrent assertion ?
Regards,
AGS