SVA for FSM

SystemVerilog
, , , ,
1

I’m trying to write an assertion to check the value of a signal ladder_value when FSM is in the below two states. This works but fails to repeat throughout the simulation. I want to have an assertion that keeps checking for the FSM to go to those two states and check for the value of the ladder_value to be equal to 8’h90 indefinitely. Please help


property ladder_values_check (rclk, fsm, ladder_value) ;
  @(posedge rclk) s_eventually(fsm == S1 || fsm == S7) ##0 ladder_value == 8'h90;
endproperty
2

In reply to nimitz_class:

Why are you using s_eventually instead of an implication?

3

In reply to warnerrs:

I need some signal before fsm to use implication, right?

4

In reply to nimitz_class:

I’m guessing you have not stated your requirements properly, so please explain why this would not work:

property ladder_values_check (rclk, fsm, ladder_value) ;
  @(posedge rclk) (fsm == S1 || fsm == S7) |-> ladder_value == 8'h90;
endproperty
5

In reply to dave_59:

It would not work because at the first posedge of rclk, FSM would be in S0, and at some point again when this assertion is triggered, FSM will be in a state that’s not S1 or S7. I want to check for ladder_value to be equal to 88 only in S1or S7 or both

6

In reply to nimitz_class:

Similarly, I have to write two more assertions to check for ladder_value to be 90 and d0 in various other fsm states

7

In reply to nimitz_class:

Dave’s property only activates when FSM is in S1 or S7. When the FSM is S0, the check does not happen. Maybe you need to provide more detail about your problem.

8

In reply to warnerrs:

I need to check for ladder_value whenever FSM goes to a particular set of states. One of those case is when fsm = S1 or S7 or both I want to check for ladder_value == 88.

Second case when fsm == S2 or S3 or S5 or all then ladder_value == 90.

And for the remaining states I want to make sure ladder_value == d0.

Hence I will require 3 assertions and they have to not fail when any of those unknown states occur. Let me know if I have to use a qualifier for that or what?

9

In reply to nimitz_class:

There is definitely some misunderstanding if you say “when fsm = S1 or S7 or both”. How can there be three choices? Perhaps you need to make a testbench showing the conditions that should pass and fail.