How to detect deadlock conditions in FSMs

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

(Originally from Issue 4.11, Item 5.0)

From: oki

I want to know if there's a method to detect the deadlock in FSM (not
in OS, but in Hardware design), when the IPs are connected the FSMs
are also connected, and if there is good ways to detect the deadlock
in SoC?

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

(Originally from Issue 4.12, Item 6.0)

From: Michal Siwinski

Recently two relatively new approaches for addressing FSM deadlocks
have been provided: Assertion-Based Verification and Predefined
Property Checking. With Assertion-Based Verification, time bounded
assertions can be used to describe the expected FSM behaviors, and in
this way, increase observability. Such assertions would typically be
expressed in terms of individual FSM state transitions, instead of
specifying complex interactions. Nevertheless, the inability to
transition out of any given state would be observed.

For example, if we know that a particular state should always
transition to another within a finite number of cycles, we can write
an OVL assertion such as the example shown below to detect a deadlock
condition:

assert_next #(0,5) fsm_read_st_deadlock_chk
(clk, rst_n, state == read, state != read);

This assertion states that within five cycles, the FSM will transition
out of the "read" state. Such an assertion can now become a target
for both simulation and formal proof with property checking.

A more automated method for deadlock verification is also available.
Several property checking tools, including BlackTie PDC, provide
automatic FSM extraction and verification of conditions such as
deadlocks. Besides not having to manually write assertions, these
tools also provide diagnosis environments that depict interacting FSMs
via bubble diagrams. The downside is that property checking will run
into size limitations and will not always be exhaustive. However,
formal property checking is quite good at finding complex corner case
bugs, making it an ideal complementary solution to simulation.

- Michal Siwinski, Verplex Systems

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

(Originally from Issue 4.13, Item 5.0)

From: Jeff Koehler

I'd like to point out the existence of IBM's RuleBase Formal Logic
Verification tool. This is now a commercially available tool:

http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/index.html

I've reviewed their web site and User's Manual for possible
introduction into our ASIC development strategy, but we aren't at a
point right now to execute an evaulation. Note: I don't work for IBM
nor do I receive any renumeration for this reply.

It appears that this is exactly what you are looking for -- automatic
identification of deadlock/livelock states. The problems arise from
the state space of most modern designs; it is too big for (our)
servers.

In order to reduce the state space, you usually:
1) run the tool on sub-sections of the full design (your designers
did perform logical partitioning, didn't they?)
2) introduce a modeling language (EDL) which restricts the tool
to only traversing paths of interest (i.e. valid situations).

Recognizing the tradeoff between complete state evaluation and useful
constraints appears to require some experience. How much experience
is what we are trying to weigh -- it will take time from functional
simulation. Note that the state of this art is not sufficient that it
can replace functional simulation.

- Jeff Koehler, Fabric Networks, Inc.