by Kaowen Liu, MediaTek Inc., and Roger Sabbagh, Mentor Graphics
Introduction
Unknown signal values in simulation are represented as X-state logic levels, while the same X-states are interpreted as don't care values by synthesis. This can result in the hazardous situation where silicon behaves differently than what was observed in simulation. Although the general awareness of X-state issues among designers is good, gotchas remain a risk that traditional verification flows are not well equipped to guard against. The unknown simulation semantics of X has two oft discussed pitfalls: X-pessimism and X-optimism[1][2][3].
X-optimism is most worrisome as it can mask true design behavior by blocking the propagation of X-states and instead propagating a deterministic value through the design in simulation, when in reality various possible values will be seen in the hardware. If the unexplored values cause the design to malfunction, then X-optimism has masked a design bug that will only be discovered in silicon.
Simply eliminating all X-states from RTL simulation is not practical. Due to power and area constraints, not all storage elements in a large design can be reset directly; some will be reset indirectly by loading values computed from other registers that have been initialized. Hence, X-states are expected to exist in the design during the start-up phase. It's important, therefore, to verify that:
- All storage elements which should be initialized (either directly or indirectly) have reached a known good state after initialization.
- Storage elements which were initialized correctly are not later contaminated by the unknown values in uninitialized state elements.
Moreover, X-states can arise in RTL simulation due to a number of other events, such as:
- Activation of an explicit X-state assignment (that was likely intended as a synthesis don't care)
- Bus driver value conflicts
- Out of range indexing
- Arithmetic exceptions
Any of these X-state values can also be masked by X-optimism and result in bugs due to simulation-to-silicon mismatches.
Using formal analysis to validated X-states has been reported as one of the industry's top five formal applications [4]. This article describes details of a comprehensive X-state verification methodology that uses automated formal methods to:
- Identify sources of X-states in the design that may not have come to light through RTL simulation
- Verify X-propagation
- Evaluate the initialization sequence
- Compute the final value of storage elements at the end of the initialization sequence to ensure they are known
- Verify that the initial values of storage elements are not subsequently corrupted by propagation of X-state values which persist after initialization or arise due to other events
There are multiple benefits to the formal approach. First, it can pinpoint the source of X-states in the design. Through static analysis of design behavior, formal can highlight occurrences of X-states that may have otherwise been masked by X-optimism in RTL simulation. Second, it can be exhaustive and deterministically evaluate all possible design behavior to determine if X-states can be propagated to corrupt known values. Third, it can employ X-accurate semantics for the propagation of X-state values, so it can defeat the X-optimism which masks true silicon behavior in simulation.
X-optimism Related Bugs
Design teams rely primarily on RTL simulation for functional verification. As discussed by Turpin [3], X-state optimism causes only one branch of conditional logic (if/case statements) to be taken in RTL simulation and thus design bugs can be hidden from view. For example, consider the multiplexing logic of the code on the following page:
Select == X
 |
In simulation, if the select signal is X, then the else branch of the if statement will always be evaluated. The X-state will be "swallowed" at this point in the design and a deterministic result will be produced. Of course, in reality, either branch of logic could be evaluated in silicon and the mux could transmit the value of either in1 or in0 depending on the true logic level of select in hardware. Since the condition where in1 is selected at that point was never tested in simulation, it creates a dangerous hole in verification coverage.
Gate-level simulation may expose some X-state issues, however, due to performance limitations, regressions are not practical and typically insufficient coverage is achieved at the gate-level. Furthermore, equivalency checking tools, which handle the lion's share of gate-level netlist verification, are incapable of evaluating the impact of X-states. Hence, an effective and efficient way to detect X-state bugs is required and is very valuable.
Sources Of X-states
Due to power and area constraints, designers often use flip-flops without an explicit reset.
always @(posedge clock)
begin
if (update && select)
reg_to_be_read <= data;
end |
The above code is an example of such a case where the reg_to_be_read flop is X-state before it is assigned a deterministic value from data when update==1'b1 and select==1'b1. Using RTL-simulation, it is hard to be confident that reg_to_be_read will always be at a valid logic level before it is used, in all modes of operation of the design. After all, it is possible that the initial X-state value is being read, but it is masked by X-optimism, so the design always produces deterministic results. Also, not all possible stimulus conditions are explored in simulation, so there may be real conditions under which the X-state is used that are either not exercised or not observed.
It is typical for data pipelines to contain X-states after the reset sequence of the design is complete. As data is fed into the pipeline, the content will gradually become deterministic, as depicted in Figure 1. So, as long as any readers of data in the datapath begin to use the data after it is written, then the initial X-states are not a problem.
Figure 1. Data Pipeline
 |
On the other hand, control logic storage elements (e.g. FSM state registers) are typically reset by the end of the initialization sequence, usually through an explicit reset, and they should never be corrupted by X-states in the datapath. The same is true for clock and reset signals.
An X-state value can also be unintentionally introduced into the design due to a coding error. For example
reg [9:0] w_slot;
assign y_data = w_slot[x_select[3:0]]; |
In this code snippet, the designer used a 4-bit signal to select one element of a 10 bit vector. If the value of x_select ever exceeds 9, then y_data will be assigned the value of X. Once again, if that happens, the propagation of the X-state may be blocked by X-optimism and it would not cause any observable effect in simulation.
Questa X-state Verification Flow
The Questa X-state verification flow is depicted in Figure 2.
Figure 2. Questa X-state Verification Flow Diagram
 |
The primary inputs to the flow are the design's RTL code and the initialization sequence. No manually generated assertions are required – they are generated automatically.
There are two steps and two groups of outputs:
- Automatic formal analysis produces results showing sources of X-states and X-propagation assertions
- Formal model checking runs on the generated assertions and produces results showing occurrences of X-state propagation
Automatic Formal X-checks
Automatic formal checking tests a design to discover how X-state values can arise. It operates directly on the RTL design, with little or no additional input required from the designer, and it finds all the common sources of X-states described above.
For example, consider the case of the out-of-range bit select of the w_slot vector mentioned above. Figure 3 depicts how this problem would be presented to the user in the tool for debug.
Here, it can be seen how the tool derived the design state where x_select is 10'h00C, which exceeds the range of the w_slot vector, and y_data became X-state.
This is an example of how an unexpected source of X-state could be debugged from the design. However, as stated earlier, not all X-states can be eliminated, as in the case of the data pipeline, and furthermore, it's possible that the designer may incorrectly waive occurrences of X-states that they assume are benign. For example, in the case of the X-state in the y_data signal above, the designer may expect that this X-state is never used by any downstream circuits, so it is allowable at this point in time. The next step in the flow then, is to verify that X-states do not propagate from X-sources to design elements that are initialized to deterministic values and should never be corrupted, such as control logic registers or design outputs.
Figure 3. Automatic Formal Debugging
 |
Formal X-propagation Checks
We now move to step 2 of the flow, where we utilize the generated X-propagation assertions from step 1. These assertions are generated for all storage elements that are correctly reset to a known good value at the end of the reset sequence and design outputs. They are very simple checks, of the form:
!$isunknown(signal_to_check) |
This assertion states that the signal to be checked should never be unknown.
These assertions are now verified against the design using model checking engines. As mentioned previously, these engines can analyze the design for X-propagation with X-accurate semantics. Here's an example of a circuit which uses the signal y_data shown above.
always @ (posedge clk or negedge reset)
if (!reset)
m_data <= 0;
else
if (y_data)
m_data <= ~in1;
else
m_data <= in1; |
In this design, m_data is a flop that is asynchronously reset and once correctly initialized with reset, should not be corrupted with X-state. As discussed, the X-state in y_data would not propagate to m_data in simulation due to X-optimism. However, formal can highlight how the state of m_data could actually become unknown. Figure 4 depicts how this is displayed to the user.
Here it can be seen that y_data goes X-state and in the subsequent cycle, formal analysis determines that m_data should also be X. In simulation, m_data would have taken the value of in1 as the else branch in the logic would have been evaluated.
Figure 4. Formal X-propagation Debugging
 |
Results And Conclusions
Unknown state signal values will always be there, but through a targeted verification approach, we can have the confidence that they will not cause functional problems. The methodology described above has been deployed on multiple projects at MediaTek [5]. It has proven to be of immense value as a supplement to simulation based verification. The results from the application of the Questa X-state verification flow to three designs are presented in Table 1. It lists the number of X-state bugs found in each block that could have been missed in RTL simulation and resulted in silicon bugs.
The automated process required very little manual effort, unlike traditional verification approaches, as neither a simulation testbench nor assertions had to be written to test the design.
Table 1. Results of the Questa X-state Verification Flow
| Block |
# Bits of DFF |
# X-propagation Bugs Found |
|---|
| A |
2357 |
2 |
| B |
14136 |
2 |
| C |
167632 |
6 |
This is just one example of how Mediatek is using formal verification in automated ways to increase design confidence.
References
- Lionel Bening, "A Two-State Methodology for RTL Logic Simulation," Proc. 36th Design Automation Conf., June 1999.
- Lionel Bening and Harry Foster, Principles of Verifiable RTL Design, Kluwer Academic Publishers, May 2001.
- Mike Turpin, "The Dangers of Living with an X (bugs hidden in your Verilog)", Version 1.1, October 2003, http://www.arm.com/files/pdf/Verilog_X_Bugs.pdf
- Roger Sabbagh, "The Top Five Formal Verification Applications", Verification Horizons, October 2012
- Kaowen Liu, et al., "Using Formal Techniques to Verify System on Chip Reset Schemes", Proc. DVCon 2013, February 2013
Back to Top
