January 19, 2011 -- Adding X states to represent unknown values can provide significant benefits in RTL verification, but runaway X propagation during simulation can hide multiple bugs that are likely to show up in silicon. Current Verilog simulation tools are dependent on the quality of the test stimulus to detect X-related issues. On the other hand, formal verification excels at rooting out these bugs down to the last corner case. This is due to several inherent advantages of formal verification, especially its ability to accurately model the X behavior without the need for any abstraction so the results reflect the real hardware. First, let's review of what Xs are, where they come from and how they affect your designs.

Defining X states and their use

There are two types of Xs that we need to consider: explicit, in which the constant X is used in the RTL to simplify verification, or optimize logic during synthesis; and implicit, un-reset flops and un-driven signals, for example.

Xs have different meanings, but basically, an X is interpreted as "don't care" in synthesis and "unknown" in simulation. In RTL design, X tells the synthesis tool that it doesn't matter whether a 0 or 1 is assigned during logic optimization. In verification, X tells the simulator that a signal value is unknown.

There are many ways to use explicit X states in verification. To cite one example, you could assign the first 8 bits of a bus to known values, and the remaining bits to X. This could make sense in a situation where you know that only a subset of the bus bits will be utilized.

During simulation, un-initialized registers automatically result in unknown values. Intentionally using un-initialized registers can be regarded as an implicit X assignment and is done to avoid wasting area with initialization. Datapath buses are expensive to initialize, and by tracking X states, you can potentially ensure that a bus is not accessed before an event occurs that makes the values on the bus valid. In the code example shown below (Figure 1), the design must ensure that the appropriate address in the memory gets proper data before an attempt is made to read that memory location.

Figure 1. An example of un-initialized registers.

Finally, unintentional X states can occur if a net is not driven during simulation. If a net or register has not been written into, and it is accessed, it will produce an X.

Some designers generally avoid using explicit X states in synthesis and verification. That's because X propagation can cause inconsistencies between simulation behavior and silicon implementation. However, they do implicitly assign Xs by using un-initialized datapath registers, because setting all the registers would waste a great deal of power and area. They also don't initialize full arrays of memories, resulting in another source of Xs.

Simulation cannot easily control Xs and ensure that they propagate to observable points, or that they don't propagate to design points (primary outputs or internal nets). Depending on coding style, simulation can be overly optimistic, generating real values when signal values are really unknown; or pessimistic, producing Xs when signal values could be known. The gate-level interpretation of X can result in a synthesized design that doesn't behave as expected.

Formal verification, unlike simulation, can evaluate the design for all possible values of X at each clock cycle. It exhaustively traverses all the paths in the design, and can find corner-case conditions where Xs propagate to observable points. As such, it offers much better prospects for controlling X propagation and ensuring safe use of Xs.

Managing X propagation

X propagation is not all bad and can, in fact, be an excellent way to find bugs because if an X occurs at an observable point, you'll be able to trace back and identify where the X assignments occurred. You can then modify the design to remove the source of the uncertainty.

To observe X at an output, you need to do two things:

First, generate a scenario creating X at the source. Second, propagate X to output.

Both cases can be serious and may occur only in corner cases. Hitting the bug requires both scenarios to have been considered and actively created, or hitting upon it during random test.

Unintended X propagation, however, can prove fatal for a design. If an X propagates to a primary output, and you go ahead with synthesis and tape-out, the chip might have an unknown value appearing at the output, and neighboring logic won't be able to process it correctly. As a result, functional behavior at the gate level or in silicon may differ from what you intended in the RTL code, leading to debugging problems or even failed silicon.

When X states occur, simulation cannot check all possible combinations of values corresponding to the X states. In addition, there is no explicit testcase to test X propagation in simulation. Consequently, they will miss corner cases that cause unintended X propagation. Further, if code is not written properly, Xs can result in both optimistic and pessimistic results in simulation.

Formal solution for X propagation

With formal verification, engineers can derive the benefits of X states without the associated risks. Sophisticated formal tools excel at bug hunting thanks to the systematic and exhaustive nature of formal proofs to reflect actual, possible silicon behavior, eliminating errors caused by X optimism/ pessimism. Simulation is no match for this level of proof, right down the very last corner case, and unlike random simulation, formal verification needn't rely on chance to hit the elusive bug.

Formal verification solutions, such as Jasper Design Automation's JasperGold, have the ability to model Xs and display a trace demonstrating the effect of their propagation on user-defined target signals, identifying all the conditions under which X can be activated, propagated and detected. In this manner, you can detect functional errors not easily found in simulation, including incorrect clock-gating resulting in Xs for register values, and incorrect control logic allowing Xs to propagate to output data buses for "valid" data. This lets you identify undesired X propagation independent of coding style and identify X issues without requiring explicit properties.

Our customers find that high-capacity, high-performance formal analysis makes it possible to handle large designs beyond the block level. To facilitate ease-of-use, JasperGold features automated set-up and processing as RTL checking criteria to detect Xs at defined points, along with a combination of color-annotated waveform and source-code debugging to identify where X assignments occurred and track X propagation through the design.

As an example from a leading IC design company, well-versed in formal methods, its designers wanted a two-phase solution where the first phase would detect reachable X assignments, and provide a trace. The second phase would prove that an X could never reach an undesired point in the design, and would provide waveforms for debugging.

At this company, designers generally avoided using explicit X states in synthesis and verification because X propagation could cause inconsistencies between simulation behavior and silicon implementation. Because setting all the registers would waste power and area as described earlier, they did implicitly assign Xs by using un-initialized datapath registers. They also didn't initialize full arrays of memories which were another source of Xs entering the design.

They also ran into X-optimism problems which resulted in differences between RTL and gate-level simulation, making netlists difficult to debug. Using formal tools, there were no missed bugs due to X-optimism as it always treats Xs as 0 or 1.

Another X propagation problem had to do with code coverage where the coverage analysis indicated that a line was hit, when it actually was not, due to an X state. Simulation couldn't possibly identify all the possible values of X and so the users relied on formal methods to dig out corner cases involving X propagation.

In summary

It's clear that the detection of dangerous Xs in designs is not a trivial problem. Current Verilog simulation tools have certain limitations in detecting X-related issues due to their dependency on the quality of test stimulus. The optimal solution is to apply formal technology to detect Xs causing discrepancies between RTL and gate-level simulation.

By Lawrence Loh and Alok Sanghavi.

Lawrence Loh is Vice President of Worldwide Applications Engineering for Jasper Design Automation, Inc. Loh has been with the company since 2002, and was formerly Jasper's Director of Application Engineering. His prior experience includes verification and emulation engineering for MIPS Technologies, Inc. and verification manager for Infineon's successful LAN Business Unit.

Alok Sanghavi is Technical Marketing Manager for Jasper Design Automation. Prior to joining Jasper he was in field applications engineering with Springsoft, Inc. and Sonics, Inc. He was a senior ASIC engineer with AMD and hardware engineer with Interdigital Communications after teaching at Brooklyn's Polytechnic University.