Power-up and potential instability analysis

Verifying the absence of undefined signal states, or the conditions that cause them, in HDL designs is a critical but often complex operation. However, X states can indicate some of the most dangerous, corner case style bugs and as such their analysis is a critical component of any verification program.

The OneSpin X-Propagation Analysis app provides a robust and effective circuit analysis that highlights all the issues in a design that could lead to X state propagations without reliance on simulation test stimulus. 

Undefined and Unknown Values in Hardware Designs

In general, in both Verilog and VHDL designs, the “X” state is used to depict a signal state that is either undefined or unknown, or has been specifically set in a “don’t care” condition.

X states can occur due to a variety of reasons, many of which indicate an error condition, and once they do occur can propagate through the design. Often an X state can indicate problems with system or component reset, or gated clocking schemes.

On occasion X states may be expected and tolerated, at least for a certain number of clock cycles, and are sometimes used to track other problems. These don’t care states are caused generally by explicit X assignments, the testing of a partial reset sequence, or X states being propagated from the input ports. These situations also require verification. 

X-Propagation Analysis

X states are notorious for indicating unusual, corner case bug conditions and, as such, creating the right stimulus, which might have to control a broad range of signals over a large number of sequential operations, can be very difficult. Thus, simulation for X-propagation tracking is unreliable, as the simulation stimulus may not drive the RTL design into a state sequence that produces the X state condition. Similarly, the use of Linting tools and other mechanisms to find harmful X states often does not produce the desired result due to a variety of restrictions. In contrast, formal verification is ideal for X-propagation analysis, given the exhaustive nature of the technique.

X propagation issues are further compounded by the nature of the HDL standards that can lead to “X Optimism.” Standard Verilog, SystemVerilog, and VHDL will sometimes mask the propagation of X states through gated logic and other code where the path through the logic on which an X state would travel is disabled, a potentially optimistic scenario. For some conditions it is desirable for the X state to propagate through a logic block if is appears on the input, regardless of the other inputs and the logic design. The X Optimism level of the verification analysis requires a level of controllability to ensure that a particular X state in question is evaluated correctly, given the design.

Often, checking for X propagation with simulation is left until later in the design process during gate level simulation, with the idea that a more reliable simulation based test will be made. Formal allows this test to be shifted to earlier in the design process, which is faster and eliminates errors earlier.

OneSpin’s X-Propagation Analysis App

Packaged formal apps can provide assertions to trap potential X state conditions, and many possible bugs may be found with relative ease. The OneSpin X-Propagation Analysis App provides a robust and effective circuit analysis that highlights all the issues in a design that could lead to X state propagations. Because it is formal, it does not rely on simulation test stimulus generating the required coverage to find all X states. The OneSpin App uses 4-state-logic formal analysis, allowing for easy debug and root cause analysis. 

The app creates assertion sets that then are utilized by a formal engine to test for the reliable execution of reset and clock signals, examine design coding for common issues that lead to X states, check control logic that can mask common problems in other verification forms, plus other analysis options. 

A typical analysis sequence is performed as follows:

1. The design is checked for coding situations that indicate a possible problem that could lead to an X state, for example:

• Divide by zero
• Array access attempt that could go out of bounds
• Uninitialized signals
• Case statements with incomplete assignments
• Function that does return a value

2. The user set the –no_X_optimism flag if appropriate to set the RTL code X optimism to be the same as a synthesized netlist.

3. The X-Propagation Analysis starts with the potential X state sources and creates assertions for any register affected. It then iterates through connected signals to apply similar assertions.

4. The user is provided the option to specify conditions to customize the analysis, although this is only necessary under special design scenarios, for example, where an X state is allowed.

5. The tool then runs the formal assertion checker to detect X propagation events.

6. If an issue is found, a simulation trace is generated that highlights the problem to allow its inspection within the included debug system. This waveform trace highlights issues leveraging cause and effect tracing to quickly discover the root problem and fix the issue.

Summary

The OneSpin X-Propagation Analysis App indicates potentially dangerous issues that are often extremely hard to find, given the corner case conditions that sometimes create them. It exhaustively tracks X propagation problems without the need for stimulus generation, providing a high degree of confidence in design reliability. The app executes quickly and eliminates the tedious creation of stimulus associated with other messages. It operates on both RTL and gate level code, and covers all potential sources of X states. Furthermore, the app includes an X Optimism setting that allows the level of optimism to be controlled to more accurately track down real issues. 

The X-Propagation Analysis app is included as part of the  OneSpin 360 DV-Verify™ product. DV-Verify includes a high-performance and capacity formal verification engine that is powerful enough to run exhaustive X propagation analysis across large blocks.

Further Reading:            

• Read the white paper on formal X-propagation analsysis.
• Watch the webinar video on preventing X-related Bugs through 4-state-logic formal analysis.

This webinar explains OneSpin’s 360 DV 4-state-logic formal analysis that enables exhaustive pre-synthesis analysis of X-propagation while considering X-optimism and X-pessimism simultaneously. See how this analysis also avoids RTL-netlist mismatches at the RTL level and thus effectively eliminates the need to run gate-level simulations to check for dangerous X-propagation.