This article is an update to Lisa Pipers original posting from April 2011: X-verification: Conquering the “Unknown”
SoCs today are highly integrated, employing many disparate types of IP, running at different clock rates with different power requirements. Understanding the new failure modes that arise from confluences of all these complications, as well as how to prevent them and achieve sign-off, is important. While the issue of handling “X’s” in verification has always been there, it has become more exasperated by low power applications that routinely turn off sections of chips, generating “unknowns”.
Lisa introduces the topic of X-Verification in her DVCon 2012 video interview:
The “unknown” as it is called in digital design, is represented as an “X” logic level. This means that the signal might actually take on a value of “1”, “0”, or “Z” in 4-state logic. X values have existed in logic design forever, and are commonly used to represent the state of uninitialized signals, such as nets that are not driven, or storage elements that have no reset. “X-propagation” occurs when one of these X values feeds downstream logic, causing additional unknowns. For example, as shown below, when signal ‘a’ is an unknown value, that unknown value is sometimes, but not always, propagated to the output.
assign y = a && b;
a b output
0 0 0
0 1 0
1 0 0
1 1 0
x 0 0
x 1 x
X’s also take on a beneficial role in both synthesis and verification. Explicit assignments to an X value can signify a “don’t care” condition that grants synthesis tools greater flexibility to optimize the generated logic. The X value is also used in verification to flag illegal states, created by problems such as bus contention. Automatic formal checking tools like Ascent IIV can use these assignments to check that the illegal state cannot be reached.
Unfortunately, X’s can also mask functional bugs in the RTL due to an X-propagation interpretation hazard known as “X-optimism”. X-optimism is a trait of incomplete coding that incorrectly transforms an unknown value to a known value. “If-else” statements and “case” statements can be X-optimistic when the condition is evaluated as an X value. Simulation semantics do not propagate the X value but rather translate the unknown X value to a known value. The fact that the condition was an unknown is no longer visible – it is hidden, in a way that makes the X-propagation elusive. Here is an example:
// if-else conditionals
out_1 = 1′b1;
out_1 = 1′b0;
condition | out_1
When condition is a 1’b1, then the output is 1’b1 and when condition is 1’b0 the output is 1’b0. But notice what happens when condition is an X value. Here the X value is an “unknown”. But the output is translated to a 1’b0, and the unknown X is now masquerading as though it were definitively a 1’b0, when in fact it could have been a 1’b1 or a 1’b0, depending on how it is synthesized into gates.
While X-optimism bugs can be detected in gate-level simulation, it is slow and painful to debug there. X-optimism may also be innocuous, but still lead to differences between RTL and gate-level simulation that must be painstakingly resolved in order to achieve sign-off.
There are capabilities of existing tools that can help with X-verification. For example, RTL analysis tools like Ascent Lint will identify X assignments. Automatic formal tools such as Ascent IIV take it a step further and can verify that designated “illegal” states cannot be reached, thereby verifying that the X value will not propagate. While highly useful, this covers a relatively small percentage of X’s that might exist. In addition, four-state formal verification tools allow you to write explicit assertions to confirm that an X value cannot propagate to a specified point. However, this requires knowledge of assertion languages and the ability to completely specify the applicable behavior of the inputs, as well as the need to know every point in the design that needs to be verified by an assertion, which is highly impractical.
X-verification sign-off is not an easy problem to solve, because the mere existence of X values is not an issue. The issue is that hazardous X propagation is often elusive because it is transformed by X-optimism into supposedly known values. Moreover, X-optimism is an insidious and intermittent problem because it only becomes an issue if the X-optimized signal is being used in the design when the optimism occurs. The functional issue that results may not be detectable for many clocks after the X-optimism occurrence, and there may be multiple sources of X in its fan-in, making root cause analysis very difficult. Adding to that, if debug occurs at the gate level, simulations are very slow and the logic is not as readable as the original RTL.
What is needed is a comprehensive solution built on the existing RTL verification infrastructure that detects when the propagation of X values masks functional bugs. Real Intent is developing just such a solution, called Ascent XV. You can read more about the solutions to the X-verification problem in the DVCon2012 technical paper.
Let us know what you are doing for your X issues.