Developing Robust Finite State Machines Code With Lint Tools

As design size and complexity grows, the design verification effort grows even more. It takes significant amount of time to thoroughly verify complex control logic of a design, which is the key and the most critical component of design functionality. One of the most common design patterns in the control logic design are finite state machines. They could be designed in different styles, state and output logic encodings, being either complex or simple for design, maintenance and verification. It is important to use the “Design-for-Verification” approach to develop Finite State Machines in a concise, robust and easy-to-verify way.

RTL code linting is the well-known approach ensuring design to be compliant with the collection of industry-best design guidelines for hardware development. Moreover, linting is able to automatically extract Finite State Machines structures from the design code and reveals FSM design bugs at the earliest stages of code development.

Standardizing FSM design patterns is an important part of RTL code standardization and it is widely used in many chip design houses. Lint tools formally verify the code to comply to company standards, avoiding design reviews and manual code check. Lint tools checks various FSM code features such as:

• State Naming conventions, including maximum name length, upper/lower case, etc.
• Proper FSM isolation in design units (such as maximum one FSM for the design unit).
• Proper FSM code sequencing (such FSM states declaration right after the states definition).
• Usage of case statements in the next-state logic (avoiding “if” statements usage).
• Usage of two or three processes to describe the FSM (avoiding the error-prone one-process FSM implementation).

Lint tools automatically identify FSM code in RTL and extract FSM structure, presenting it in the FSM graph window. Designers visually approve the FSM design intent reviewing these FSM graphs. For the legacy code, extracted FSM graphs act as a design specification, allowing better understanding of the RTL code and facilitating its reuse. The following picture demonstrates the FSM graph extracted by Lint tools:

After FSM extraction, Lint tools apply various structural and functional checks to further verify FSM correctness and its compliance to company standards. For example, it is a good practice to avoid using Mealy and Mixed FSM types, preferring Moore FSM types only.  Moore FSM outputs are registered and therefore they don’t propagate possible FSM input glitches to FSM outputs. Moore FSM are preferable from a timing perspective too, as FSM output timing paths include output decoding logic only. Also, it is a good practice to enforce a specific state encoding type to better fit a design into design requirements. For example, the one-hot encoding with Moore FSM type is preferable for the high-speed designs, while Gray encoding being preferable for the low-power applications, etc.

ASIC and FPGA synthesis tools require synthesis-specific attributes to implement the FSM according to the design intent. Lint tools guarantee that proper synthesis-specific attributes accompany the FSM code.

After the FSM extraction, Lint tools functionally validate that all the FSM transitions are activatable, making possible FSM state transition from one state to another. For example, a transition such as:

if (a > 7) next = StateA;

will never be executed if variable “a” is defined with bit width of 3 or less. Otherwise, the FSM graph presents such FSM transitions as non-activatable as it is shown in the following picture:

The lack of transition activation causes the “normal” state to become unreachable or creates dynamic or static deadlock.

After the FSM transitions verification, Lint tools analyze FSM structure for deadlock, redundant and unreachable states.

Deadlock states “freeze” the FSM as they don’t have output transitions to other states. The following example shows the FSM with the deadlock “Error” state:

Having the FSM structure extracted, and all transitions verified, Lint tools check that there are no deadlock states in FSM descriptions.

As opposed to the deadlock states, unreachable states do not have input transitions, making FSM impossible to enter either one of these states. In some FSM designs, only the Reset state is allowed to be unreachable in a case that it is never used later on while design is running. The following example shows the FSM with unreachable “Ready” state:

In addition to static deadlock, dynamic livelocks may exist in Finite State Machines too. Dynamic livelock represents not the single state, but rather the group of FSM states. Once entered, the FSM cannot leave this group, continuing to circulate between the group states. The following example shows the FSM with dynamic livelock, represented by the group of states (S2, S3, S4):

The usage of Lint tools is very important for the development of the mission-critical designs. These designs should work flawlessly under any PVT (process-voltage-temperature) variations, being resistant to excessive radiation levels and aging. One FSM safety feature is the ability to restore the state machine to a safe state if the state register becomes corrupted. Lint tools provide such checks as well, making sure that there is always a default statement in the FSM branches description, and all execution branches of the default statement lead to safe state(s).

Safety-critical designs are required to be glitch-free. For example, the RTCA/DO-254, Design Assurance Guidance for Airborne Electronic Hardware, defines the set of guidelines that need to be followed in order to ensure glitch-free and safe operation of aircrafts. Making Finite State Machines glitch-free is of high importance for such designs, as Finite State Machines usually control significant parts of design logic. Lint tools help to guarantee the glitch-free operation of designed FSM logic. Designers may configure Lint tools to allow only a glitch-free types of Finite State Machines, for example:

• Moore or Mealy FSM with registered outputs.
• Moore Output-based encoded FSM.

The following pictures represent the structures of such glitch-free FSM types in more detail:

In summary, Lint tools are able to validate deadlock, lovelock, reachability as well as many other FSM-related issues at the earliest design stages, saving verification time and eliminating possible functional and implementation flaws. It is advisable to develop Finite State Machines in RTL code using their immediate static verification provided by Lint tools. The FSM extraction feature provided by Lint tools could be used to better understand legacy or third-party RTL code. For safety-critical designs, Lint tools help to ensure FSM code safety according to safety standard requirements. If you’d like to try to validate FSM-related issues, simply request a free evaluation from us of ALINT-PRO.