Enhancing Early Static FSM

Finite state machines (FSMs) are widely adopted as part of reactive systems to capture their dynamic behaviors using a limited number of modes or states that usually change according to the applied circumstances. Some terminologies are frequently used to describe the FSM characteristics: state, transition, condition and sequences. A state defines the behavior and may produce action or output; a transition describes change involving of state(s); a condition allows transition to occur; and a sequence is comprised of a set of two or more transitions.

FSM can be categorized in term of its output transition. A deterministic FSM, if it has only one transition to next state; while a non-deterministic FSM has more than one possible next state for each pair of current state and input vectors. For practical applications, FSMs can be grouped based on how their outputs are defined. Moore FSM is the state machine whose output are a function of the current state only, while a Mealy FSM has its output and next state dependent on both the current state and input(s).

Many of the FSM practical applications such as in communication systems, crypto-processing, visual processing and as part of the embedded controllers are implemented using various schemes, from a static to be more reconfigurable styles –depending on if it is internally initiated (self-reconfigurable) or driven by external reconfiguration events.

Aldec and Verification of FSM
As an industry leader in Electronic Design Verification, Aldec’s solutions include a verification strategy in ALINT-PRO™ that is comprised of three key elements: static structural verification, design constraints setup, and dynamic functional verification.

The first two steps are executed in ALINT-PRO, while dynamic checks are implemented via integration with Aldec’s simulators Riviera-PRO™ and Active-HDL™ (ModelSim® is supported) based on the automatically generated testbench.

Previously, designers had to deal with debugging the FSM late in the implementation stage such as by using Riviera-PRO advanced verification platform as illustrated in the following diagram:

“Most issues designers face when implementing FSM-based control blocks tend to be caught during RTL-signoff, using coverage-enabled simulation and/or formal property checking methods,” observes Sergei Zaychenko, Aldec Software Product Manager.

In response to the increasing verification challenges for complex designs, Aldec has expanded the rule-checking capabilities of its popular ALINT-PRO™ tool. it has enhanced the tool to include twice as many FSM checks and new graphical representations to aid with state explorations.

“Aldec ALINT-PRO can discover many complex FSM issues long before test stimuli are available. With the latest version of ALINT-PRO™ users can do FSM-level verifications that will save them a significant amount of verification time further on down the line,” added Sergei.

An early FSM static validation can be achieved with ALINT-PRO by taking a two-step approach: first by performing an FSM exploration using FSM graphical environment, and then by applying a complete list of FSM targeted rule checks. ALINT-PRO extracts FSM from a design code and presented in FSM viewer.

To facilitate a better exploration of the extracted FSMs and reveal FSM-based design issues, ALINT-PRO (v2018.07) has an enhanced GUI incorporating checks based on the 25 newly added FSM design rules covering advanced aspects and typical errors. The FSM window acts as the FSM debugging tool that generates state transition graph with color-coded notation signifying transitions among object states. It differentiates a deterministic, non-deterministic, beginning and ending state. Designer could trace a sequence and switch data representation mode from graph to tabular format.

FSM Static Checks and Coding Issues
An event-driven system programming tends to use heavily nested conditional constructs (if-else, switch-case) in order to implement various responses due to a triggering event or a combination of past events in the system. FSM adoption is intended to reduce potential clutters caused by the complex number execution paths, the multitude of variables and the many transitioning between different modes of execution.

ALINT-PRO identifies FSM related bugs including unreachable, deadlockand redundantstates which are the common types of shortcomings faced by designers while capturing the FSM RTL codes. An unreachablestate is not reachable from any initial state of the FSM but has output to transition; while a deadlockstate is reachable but once entered indefinitely unable to change its state; and a redundantstate has neither input or output transition from/to.

The FSM type compliance check can be targeted to a pre-defined set of requirements such as to satisfy two combinational and one sequential processes. Additional FSM implementation specific checks such as those related to reset control, FSM state enumeration, state encoding type allocation (binary, gray, onehot, etc.) and other FSM attributes declaration (e.g., fsm_encoding=…) are complementing the over 40 new rules designated for improving the VHDL and Verilog/SystemVerilog RTL coding quality.

To generate a highly reliable design, best-FSM-design-practice type of checks can also be applied. This includes good naming conventions (describing more than one FSM in a single design unit, unique names for states of different FSMs, etc.); FSM should recover in Reset state in case of FSM state variable corruption and use case default with unconditional transition to FSM reset state. Reset state transition handling is crucial such as in autonomous sequential modules of a complex digital system.

Workspace, Project and Heterogeneous Design
In ALINT-PRO environment, the RTL codes, constraints and properties are captured into workspace and projects. An enhanced setup automation for complex Xilinx Vivado and ISE projects is made in 2018.07 release. The extension enables a “push button” flow for early static verification of IP-intensive Xilinx FPGA-targeted designs. A workspace is automatically organized to deliver hierarchical and incremental DRC and CDC analysis, allowing the designer to concentrate on checking custom RTL blocks, while preserving accuracy at the boundaries of IP blocks. Unless an IP block is re-configured in the original design environment, it is only being analyzed once, and the extracted block-level timing constraints are automatically promoted to enable higher level verification of the main design.

To find out more about ALINT-PRO, please check HERE