OVL assertions: state machine check

[chainastole]

I desire to place OVL checkers on the FSM transitions. I wanted to use
the "assert_transition" checker, defining the FSM current state as the
test expression; a specific value of the current state as the start
state and an expression, describing the transition as the next state.
This expression depends on the input signals, updated during the work.
The problem is that the evaluation of the expression for next state is
performed on the exit from reset and any further change of the
expression doesn't influence the expression evaluation, in other words
the assertion seems to handle only non-changing expressions.
This restricts my possibilities to check the FSM.
What should I use to nevertheless check that if in the middle of the
work the signal "A" appears the FSM transits from the "CURR_STATE" to
"NEXT_STATE_A" and if signal "B" appears, it will transit to
"NEXT_STATE_B"?

 

[Srinivasan Venkataramanan]

Hi,
It has been a while since I looked at OVL, so I am not sure why
assert_transition should be limited to constant expressions. In SVA/PSL, it
is straightforward to do what you wanted. I believe VCS's SVA Checkerware
library can handle it too - so if you use VCS, just by simply pointing to
our SVA Checkerware library (instead of OVL) you will get this functionality
(if I'm not wrong) and much more coverage insight into the same.

Can you post a simple-but-complete example code and show us why you think
OVL isn't doing the job for you?

Thanks,
Sri

--
Srinivasan Venkataramanan
Co-Author: SystemVerilog Assertions Handbook, http://www.abv-sva.org
Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition.
http://www.noveldv.com
I own my words and not my employer, unless specifically mentioned

 

[chainastole]

Spasibo.

 

[Alexander Gnusin]

"chainastole" <chainastole@yahoo.com> wrote in message news:<1108992399.978568.16390@o13g2000cwo.googlegroups.com>...

I desire to place OVL checkers on the FSM transitions. I wanted to use
the "assert_transition" checker, defining the FSM current state as the
test expression; a specific value of the current state as the start
state and an expression, describing the transition as the next state.
This expression depends on the input signals, updated during the work.
The problem is that the evaluation of the expression for next state is
performed on the exit from reset and any further change of the
expression doesn't influence the expression evaluation, in other words
the assertion seems to handle only non-changing expressions.
This restricts my possibilities to check the FSM.
What should I use to nevertheless check that if in the middle of the
work the signal "A" appears the FSM transits from the "CURR_STATE" to
"NEXT_STATE_A" and if signal "B" appears, it will transit to
"NEXT_STATE_B"?

The usage of "assert_transition" is limited, especially for FSM
checks. "assert_next" is the better choise, such as:

assert_next #(1,1) trans_A (clk, reset_n, (state==CURR_STATE & A),
(state==NEXT_STATE_A));
assert_next #(1,1) trans_B (clk, reset_n, (state==CURR_STATE & B),
(state==NEXT_STATE_B));

Regards,
Alexander Gnusin