Hello SVA Experts,
The design state machine is having lets say 4 states, S1, S2, S3 and S4.
From S1 I can reach S2, S3 or S4 (Only 1 of them shall be True at any given time)
S1 to S2 is single clk cycle state transition.
S1 to S3/S4 may be multiple clock Cycles (this can vary).
I have coded initially as below.
@(posedge clks) disable iff(~POR_N)
(state === S1) |=> (state === S2) || (state === S3) || (state === S4);
option1: This passes for all cases.
(state === S1) |->##[1:$] (state === S2) || (state === S3) || (state === S4);
first_match((state === S1) |->##[1:$] (state === S2) || (state === S3) || (state === S4));
Please suggest if these options are right to use.
Also there is a very common requirement that when reset is applied, there is a default state say S1 in the above case. As there is no clock involved how do we write an assertion for this?