Introduction

The use of unknown values (X states) can provide significant benefits in RTL verification, and can allow better logic optimization for synthesis. But uncontrolled or unexpected X propagation in simulation can also mask bugs, potentially leading to failures in silicon. Simulation alone cannot adequately simulate and observe all X states. Formal technology can provide a much more complete solution that allows engineers to derive the benefits of X states without the associated risks.

Simulation cannot easily control Xs and ensure that they propagate to observable points, or that they do not propagate to design points (primary outputs or internal nets) where real Boolean values are expected. 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 both possible values of X (0 and 1) 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. What’s needed now is an approach that eases the burden of writing specifications, helps users easily debug problems, has high capacity, and uses industry-standard specifications that support portability.

This paper will draw upon experience from ARM and AMD to show how X states are used in synthesis and verification. It will show how simulation and formal verification handle X propagation today, and outline some of the requirements for an ideal solution based on formal technology.

What X states are and how they’re used

Different semantics are associated with X for different parts of the design flow. 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 three basic sources of X. The first of these is an explicit assignment of X in logic optimization, which allows the synthesis tool to choose either a 0 or 1 to improve logic minimization. This can have unintended consequences during verification, such as the X-optimism or X-pessimism described in the next section.

In the second case, X is explicitly assigned for verification purposes. For example, you could have a case statement in which four cases are enumerated – 00, 01, 10, 11 – and then have a default to which you assign an X. These Xs appear in RTL code as 1’bx. They are added to the RTL to uncover unwanted conditions. For example, if a selector signal that should be one-hot is not because of incorrect or uninitialized logic, the case statement goes to the X default and is propagated towards an observable output (see Figure 1).

Figure 1: An example of an explicit X assignment (a) to detect non-one-hot values of “busSelect” and (b) to detect unknown values on “busSelect”

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.

In the third case, uninitialized registers automatically result in unknown values in simulation.  Intentionally using uninitialized registers can be regarded as an implicit X assignment. It is often done to avoid wasting area with initialization. Datapath busses 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, the design must ensure that the appropriate address in the memory gets proper data before an attempt is made to read that memory location.

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.

Engineers at ARM 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 uninitialized datapath registers, because setting all the registers would waste a great deal of power and area. They don’t initialize full arrays of memories, and that’s another source of Xs coming into the design.

ARM uses assertions that check for undesired Xs. For example, the company’s coding guidelines say that there should be an X default for every case statement, and assertions check to see whether the default case is ever hit. Assertions also check the requirement that AMBA bus signals should never be Xs.

At AMD, engineers use X states in synthesis so that optimization can produce the smallest possible circuit. This helps save area and power, and improves routability. But it can potentially result in ambiguities that cause discrepancies between RTL and gate-level simulation.

Because of the difficulty of debugging X propagation, AMD engineers generally avoid generating Xs from testbenches. AMD also generally discourages the use of uninitialized registers, but does allow a certain percentage to be uninitialized in order to conserve real estate. Designers are encouraged to use assertions to ensure that uninitialized registers don’t flood the design with unwanted Xs.

Managing X propagation – where simulation falls short

It should be noted that X propagation is not necessarily a bad thing. If it’s intended, it can be a powerful tool for catching bugs in a design. Ideally, if an X occurs at an observable point, you’ll be able to step backwards and identify where the X assignments occurred. You can then modify the design to remove the source of the uncertainty.

Unintended X propagation, however, is a problem. If an X propagates to a primary output, and you go ahead with synthesis and tapeout, 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 0 and 1 corresponding to the X states. In addition, simulators can’t run enough scenarios to catch all X propagation issues. 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.

X-optimism occurs when the interpretation of X takes just one if/case branch when many should be considered1.  It thus produces a binary value of 0 or 1 when the actual state is unknown. You might have monitors set-up to check for Xs at points where they should not occur, but due to X-optimism, the Xs are blocked. As a result, the behavior of the netlist and/or silicon implementation will differ from the RTL.

An example of X-optimism is as follows:

Suppose a reachable don’t care X is assigned to CountEn. The else/if branch will only execute if CountEn is 1’b1, so no update occurs if CountEn is X, and the count will keep its previous value. Effectively, the simulator is treating the X as a 0 when in reality it could be either a 0 or 1.

X-pessimism occurs when results lead to more X propagation than is really necessary. It thus generates Xs where there are actually binary values. X-pessimism is demonstrated in the following example:

The simulation interpretation of the assignment is:

assign status = (sel & statusA) | (~sel & statusB);

Suppose statusA and statusB have equal values, say 1’b1 or 1’b0. In simulation, when sel is set to X, the value of status is always evaluated as 1’bX. In reality, status should be equal to statusA and statusB regardless of the value of the select line.

X propagation issues at ARM and AMD

ARM engineers have run into problems with X optimism, and the company has developed coding guidelines to avoid it. For example, the guidelines generally prohibit the use of if statements, which can block Xs, and casex statements, which can result in X optimism if they’re used with overlapping terms.

ARM has observed that X optimism can result in differences between RTL and gate-level simulation, making netlists difficult to debug. Such differences can also occur when memories propagate Xs back into the design. The synthesis tool may or may not propagate these Xs into the netlist.

Another X propagation problem noted by ARM has to do with code coverage. The coverage analysis may say that a line was hit when it actually wasn’t, due to an X state. ARM has also noted that simulation can’t possibly simulate all the possible values of X. This is why ARM relies on formal technology to dig out corner cases involving X propagation.

AMD has run into problems with X optimism and X pessimism, and engineers have observed inconsistencies between RTL and gate-level simulation as a result2. For example, they’ve noted that if a select signal is X, a NAND gate implementation of a multiplexer will produce an X if the inputs are 01, 11, or 10. This is an example of X pessimism, because real silicon will produce a 1 when two inputs are 1s.

Recently, AMD noticed a new problem with X propagation. One block may be generating garbage data because the values are “don’t cares.” But another block cannot stop or ignore the garbage, because it contains optimized parity logic. Xs then travel freely and assertions written to detect them fire, halting the simulation.

One solution is to place a “guard” that prevents the second block from reading garbage data. In this case, however, engineers are creating hardware to deal with Xs, which do not exist in the real world. The other solution is to go back to synthesis and generate only 0s and 1s in extreme cases where Xs would cause unwanted propagation.

AMD has also noted that low power design can cause problems with Xs. For example, suppose an engineer places a gated clock on the input to an AND gate. If a control input goes to X, the AND gate will produce 0Xs and X0s. Verilog simulation will treat 0X as a rising clock edge and X0 as a falling clock edge. It may look like nothing is happening even though the clock is still running.

AMD engineers write assertions to detect Xs on all important interfaces between blocks. But the company has found that it’s very difficult to write assertions and tests that can flag all possible X propagation scenarios. AMD sees formal verification as a solution because it can explore the whole design space, consider all possible X assignments, and trace the propagation of Xs to unwanted locations.

How formal technology can help

In contrast to simulators, formal property checkers consider the sequential behavior of a design, tracking all possible values of Xs through internal registers. They can go through all the paths of a design and show if an X is going to propagate to an observable point – or propagate to an unwanted primary output. In addition to the more complex problem of X propagation, formal tools can also check for reachable X assignments. However, reachability of an “X-assignment” does not guarantee an X state will propagate and terminate correctly.

Let’s review the examples we just used of X-optimism and X-pessimism and see how formal technology would make a difference. In the first example below, formal analysis will try both 0 and 1 values of CountEn, as opposed to treating an X assignment as a 0.

Figure 5: Formal verification (FV) analyzes design for both possible values of X.

In the following example, when the select line is set to X and statusA and statusB are both 1’b1, a formal tool will properly assign a 1’b1 to the status line. A simulator, as noted in the previous section, would assign an X to the status line.

assign status = (sel & statusA) | (~sel & statusB);

ARM uses formal verification because formal tools try 0s and 1s for all Xs. They also provide reachability analysis, which AMD finds useful for back-end quality checks on code coverage. ARM has developed its own scripts to do a sequential comparison using commercial formal model checking tools. This comparison can take two versions of the design and run full model checking sequences to check for X differences in the outputs. The current approach has resulted in some capacity challenges, however, and it requires design partitioning.

AMD uses existing formal tools to detect reachable X assignments. The company has noted some limitations with this approach. Generating constraints is not easy, and reachable X assignments can still cause problems. AMD would like to see a more automated solution that doesn’t require a large number of constraints.

Towards an ideal solution

An ideal solution for safe X handling would go far beyond a quick check for unreachable states. It would use formal technology to identify all the conditions under which an X can be activated, propagated and detected. It would thus search for all possible ways X can occur in a design.

This ideal solution would identify undesired X propagation independently of the user’s coding style. In some cases, it would not require the user to write properties. When properties are needed, they could be written using Xs.

Debugging is an important part of any X handling solution. Ideally, debugging would help users to quickly get to the root of the problem, without being overloaded with too much information. A combination of color-annotated waveform and source-code debugging would let users identify where X assignments occurred, and track X propagation through the design.

ARM would like to see an X handling solution that will run without requiring a lot of scripts, and will provide a “pushbutton” analysis that won’t require writing assertions. Debugging is also important. The solution should be able to track where Xs came from in the RTL.

AMD would like a two-phase solution that first detects reachable X assignments, and provides a trace. Illegal traces can be eliminated by adding more constraints, or by conducting a formal analysis to find out if the traces of interest can be generated by the real RTL code that feeds the design under verification. Next, it would prove that an X could never reach an undesired point in the design, and it would provide waveforms for debugging. The solution would trace Xs from their origins to their outputs, ensuring that unwanted X propagation does not occur.

Conclusion

The proper use of Xs is an important topic in verification, but it has drawn little attention. It’s time for more awareness about how Xs can be safely used, what the advantages are, and where the risks lie.

Simulation alone is not sufficient for controlling and predicting X propagation. It cannot check all possible values of X, and may report optimistic or pessimistic results. Formal technology offers much more potential for eliminating undesired X propagation and ensuring desired propagation. An ideal solution would employ formal tools along with a comprehensive X analysis and a user-friendly debugging environment.

Reference

1. Mike Turpin, ARM Ltd., “The Dangers of Living with an X,” October 2003
2. Christian Hauf, Frank Rogin, AMD Inc., “Ad-Hoc Translations to Close Verilog Semantics Gap,” DDECS'2008, Bratislava, Slovakia, April 2008

Rajeev Ranjan is the chief technology officer of Jasper Design Automation and is responsible for developing Jasper’s overall technology vision. Prior to joining Jasper, Rajeev was CTO and VP of Engineering at Real Intent, where he led the development of their products and set the company’s technical direction. Rajeev has been active in the area of formal verification for over 15 years and has published numerous articles and holds a number of patents in the area of functional verification.

Yann Antonioli is product manager at Jasper Design Automation. He joined Jasper in 2003 and is currently managing JasperGold Verification System and other products. Yann has been working in the field of formal verification since 2001 when he joined Verplex Systems. Prior to that, he worked as a digital and analog designer and test engineer at Sharp Corporation in Tenri-shi, Japan.

Alan Hunter is design verification methodology lead at ARM. His main interest areas are formal verification, functional coverage, and design verification process optimization. He is co-author of Verification Methodology Manual for SystemVerilog.

Oleg Petlin is a verification manager for AMD, where he focuses on formal verification methodologies.  In addition, Oleg’s interests include design for testability, functional verification, and verification management. Before joining AMD, he was a director of verification at SiCortex, Inc.