Clocking event in Concurrent Assertions

SystemVerilog
, , ,
1

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

2

The problem is when your <property_expression> contains a reference to ps_state. Because of sampling semantics, it will have the old state, not the new state.

You could put your assertion into an implication

$changed(ps_state) |-> <property_expression> ;
3

Hi Dave,

Yes, when using ps_state as clocking event I call a subroutine to return the new ps_state and use it as part of property_expression

From SV LRM perspective above logic works as per intention.

I was curious whether it would work / considered legal for formal tb as well