FSM Verification

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 3.15, Item 9.0)

From: Ben Cohen

1. How do you verify that an FSM cannot possibly go into a deadlock
situation, and never get out of it? Which tools do you use, and
were you successful (i.e., did it ever uncover issues)?

2. How do you verify that an FSM is safe, and should a glitch or
single event set occurs the FSM gets out of its abnormal
condition?

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.1, Item 8.0)

From: Jeff Li

When addressing such FSM problems, the size of the FSM is a critical
factor. These questions are about all state transitions. 30 state
variables make 1 billion states. 30 input bits make 1 billion
transitions per state. Simply going through all these state
transitions at the speed of 1 billion state transitions per second
will take more than 10,000 days.

Model Checking is made to handle these problems. Some results from the
oldest (and still very active) model checking research group can be
found at http://www-2.cs.cmu.edu/~modelcheck/pubs.htm including some
papers in pdf format. It works well if the FSM is not too large. Any
FSM with close to 10,000 state variables is usually too large. This
should not be a problem with the above 2 questions because there is no
need to consider how a small FSM interacts with the rest of the
design. Most FSM sizes in RTL source code are much less than 100 state
variables.

However, most other verification issues are not so lucky. Model
Checking has been used (or experimented) widely at IBM and many other
places. A good collection of information is at
http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/about_rulebase.html

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.1, Item 8.1)

From: Flemming Hansen

This can be done with a static functional verification (SFV) tool. You
could write a property for each state, saying that if the design is in
this state, if is not true that it will also be in this state in the
next cycle. Note that this is different from saying that the design is
not in this state in the next cycle.

> 2. How do you verify that an FSM is safe, and should a glitch or
> single event set occurs the FSM gets out of its abnormal
> condition?

With a SFV tool you would simply list the legal states, and then write
a property stating that if the design is in a legal state, it will be
in a legal state in the next cycle, and if the design is in an illegal
state, it will be in a legal state in X cycles.