Formal Verification SVA assume signal to NOT toggle at negedge

SystemVerilog
, ,
8

In reply to ben@SystemVerilog.us:

Hi Ben,

The reason for constraining this signal is because it is messing with my helper FSMs. The next_state (being driven by combinational logic) would jump all over the place if this signal is not stable at the negedge.

For now indeed I am forcing the signal (with the following) to be high for 2 or more cycles but that snips out a portion of the valid state space.


ASSUME_FullCycle: assume property (@(posedge CCLK)
  sig
    |->
  sig[*2:$]
);