Randomizing 9 bit signal to be one hot and stable for the entire simulation in Formal verification

SystemVerilog
, , , ,
1

I’m trying to write a constraint on a 9 bit signal to be one hot and stable for the entire simulation using FPV:

Assume_Signal1 : assume property (@(posedge CLK) disable iff (Reset) ##1 $stable($onehot(Signal1)));

Giving this above constraint, I’m seeing Signal1 changing every clock cycle which isn’t expected. Could someone clarify the gap in the logic?

2

In reply to Arslan Naval:

Did you mean to write the boolean expression $stable(Signal1) && $onehot(Signal1)?

3

Intent is what you mentioned but giving " $stable(Signal1) && $onehot(Signal1)" would cause an issue right? Just coming after reset Signal1 would hold ‘X’ or any random value because of $stable(Signal1).

4

In reply to Arslan Naval:

Because of the ##1, it’s the second clock cycle after Reset that $stable gets evaluated. That implies that Signal is one-hot in the first clock cycle after reset and never changes.