Ensuring that code segments can be activated
Deadlocks in finite state machines, unreachable code and stuck signals are major concerns when developing and integrating RTL components. Usually they point to functional errors or misinterpreted integration conditions that render certain design functionalities inactive. These might include miscalculated branching conditions, incorrect wiring, or interlocking conditions. These errors cannot reliably be detected using simulation, which can only demonstrate the activation of certain design functions, but can never prove the opposite case, the inability of such designs to be activated.
OneSpin’s Activation Checks App automatically checks for activation of particular common design functions, for example if code can be reached, transitions of finite state machines can take place, and if signals can assume all desired values.
Formal Un-Reachability Analysis
Formal is the only technology that can prove the absence of capability, that is, it is able to show that it is impossible to activate some function, i.e. proving it is unreachable. This information is useful both for debugging these conditions, as well as creating coverage waivers for simulation if the function is indeed not relevant in the context of the design. If it is possible to activate a function, a formal approach will find out and construct a sequence of stimulus that demonstrates the activation. The generated trace can then be used for the interactive analysis of design behavior, or the creation of a simulation test bench.
The Activation Checks App is a powerful design analysis tool that automates the creation and execution of formal checks for activating particular common design functions.
The app can perform three classes of checks:
- Dead-code-checks that target each branch of input source code, and check whether the branching condition can be activated. Both if-then-else and switching conditions are considered, and the default behavior is analyzed. This is particularly helpful to avoid don’t-care conditions, via explicit X-assignments, that could lead to simulation synthesis mismatches and other hazards.
- Finite State Machine (FSM) checks verify that each transition of an FSM can be performed, that no dead-locks exist, and that the machine is correctly returning to an initial state on reset. FSMs are automatically identified in the input source code. The checks are performed across the entire design function, and include other FSMs that might interact with the machine under consideration. This is particularly helpful for finding unwanted inter-locking conditions between multiple FSMs.
- Toggle-checks analyze the switching capability of signals in the design. The checks performed depend on the type of the signal. For example, in case of a Boolean signal, they check whether it can transition from 0 to 1, and from 1 to 0. For other signal types such as numeric and enumerated signal types appropriate checks are applied. Outputs and state holding signals are verified by default, while checks for other signals can be created on demand.
The three classes of checks provide a flexible way to point out different design issues, as often they could expose similar problems in different ways. For example, an enumeration signal stuck at a certain value could have the same cause as a dead-lock in a corresponding finite-state-machine. This allows to target issues from different angles, easing root cause analysis. To target different problem classes and different design areas, the user can control individual checks, and the tool can be directed to analyze specific questionable design sections.
Common Use Models
Activation checks are most efficiently used during early design stages, and later for IP validation and integration:
- During early design stages the app can be used efficiently to analyze newly written design functions. If a function cannot be activated, it suggests incorrectly coded execution and branching conditions.
- During IP validation and integration, the app exposes if design functions can no longer be activated after integrating a block, which suggests a problem with the assumptions regarding the integration conditions, wiring, etc.
The Activation Checks are easy to use, as the only input is the RTL code. Due to the nature of the checks, the tool will never produce false positive results in terms of reporting unreachability, dead locks, etc. The reachability traces can be further refined by adding additional environment constraints, such as those from the Protocol Analysis App. Any activation problems can be displayed in the debug environment with the app generating a witness that reveals the source of the issue. In addition, special displays for FSM deadlock and other conditions are available.
The number of activation conditions that need to be analyzed to ensure correct design operation can be large. Therefore, special care has to be taken to ensure scalability. The Activation Checks solve this problem elegantly by automatically grouping related checks, and executing multiple check groups concurrently across the network, and even leveraging cloud-based engines. This scalability allows the app to be used interactively during design entry, up to large block integration analysis. Special prove engine heuristics for the Activation Checks fully leverage the power of the entire OneSpin formal verification platform.
The Activation Check App operates on all common language standards, including System Verilog, VHDL, as well as SystemC/C++. The app leverages the full easy start and debug systems available in the OneSpin DV product line.