Finite state machines: How to debug and verify them early in the flow

Finite state machines (FSMs) are a familiar and frequently used technique in electronic systems design, yet can still prove sources of error. FSM deadlocks and unreachable states are the most common.

The good news is we know so much about FSMs that we can apply dedicated RTL checks and debug them early in the design flow. With the right tools, it is relatively easy to catch FSM errors before fixing them becomes costly and time consuming.

What are finite state machines?

An FSM represents a straightforward way of reducing the number of flip flops in your design. FSMs can enter a series of defined states – but only hold one at any time – depending on a particular set of inputs.

An ATM provides a real-world analogy for the way that finite state machines work. Entering your PIN at the ATM provides access to your account. You then input how much money you want. Assuming the funds are available, they are dispensed. Ejecting the card then resets the process, ready for the next customer.

An ATM is a large-scale example of a finite state machine (Adrian Grycuk)

This simplified ATM process highlights an important rule of thumb for implementing FSMs in logic. Reliability and security are best achieved by keeping FSMs as simple as possible. They can be designed with multiple ‘state’ targets, but the more there are the greater the risk of creating deadlocks and unreachable states.

For our ATM analogy, we could design one FSM for PIN verification, one for capturing and verifying the funds entered, and a third for card return and reset. This should increase the reliability and security of the implementation, although we would also need to ensure valid hand-off from one FSM to the next.

What can go wrong with finite state machines

A finite state machine deadlock occurs when the RTL describing the FSM has been generated in such a way that, once the FSM has entered a particular state, there is no valid input that will trigger its exit from that state.

Unreachable states are created when a designer creates a state as part of the FSM, but there is no combination of inputs that will lead to that state. The threat here is of implementing logic on the chip whose behavior includes unknowable outcomes.

Verification and debug of finite state machines

You can generate your own assertions to check that FSMs perform as intended. Similarly you can try to pick them up during a full functional verification run. However, while individual FSM bugs are often easy to fix, they are likely to be deeply embedded in the RTL, particularly given their fundamental functionality. They can therefore often be missed during traditional simulation.

However, FSMs are now such an established part of design that related EDA tools leverage a lot of accumulated knowledge to apply automated checks quickly as RTL becomes available. No testbench is required.

One example is the Ascent IIV Autoformal tool from Real Intent.

The tool conducts a hierarchical analysis of the overall design and then generates a set of functional assertions that cover not only FSM issues, but also those associated with areas such as bus contention, X-propagation, dead code, pragma violations and more.

This hierarchical approach helps Ascent IIV Autoformal identify bugs that are more deeply embedded by directly targeting the design’s original intent. The emphasis is on early identification of any issues.

Having diagnosed any FSM issues within the RTL, the tool generates debug reports including traces back to any erroneous state-transition assignments. Smart reporting of the incidence and also the depth of any problems makes for earlier and easier repair.

In addition to bus issues, the Ascent IIV Autoformal package also runs checks for:
• Bus contention and floating bus issues
• Full- and parallel-case pragma violations
• X-value propagation
• Array bounds
• Constant RTL expressions, nets and state vector bits
• Dead code
• SystemVerilog ‘unique’, ‘unique0’, and ‘priority’ checks for ‘if’ and ‘case’ constructs

Beyond the challenge of finite state machines

Much of what has been discussed here will be known to you. In many ways, that is the point. Familiarity does breed contempt.

Design techniques like FSMs remain frequent sources of bugs, despite the fact that they are so widely understood and used. FSM bugs are often the result of, say, overloading an FSM or even a simple typo. These are familiar errors, but are still complex and expensive to fix if they are identified only late in the verification flow.

The increasing ability of tools to view the design intent hierarchically and to apply an ever-growing knowledge of how various techniques should work means that many types of bug can be tracked and fixed before a design enters a lengthy phase of simulations.

This ‘divide and conquer’ approach to complex SoC verification can help counter the increasing complexity of SoC verification, enhance productivity and accelerate time-to-sign-off for electronics system design.