X-Propagation in RTL: How Formal Verification Finds Reset and Unknown-State Bugs

An RTL simulation can finish reset, run thousands of tests and still hide a control bug caused by an unknown state. The problem is not simply that an X appears in a waveform. The important question is whether uncertainty from an uninitialised register, reset sequence, invalid selection or power-state transition can reach logic whose value matters to the behaviour of the design.

The key takeaway is this: formal X-propagation analysis can complement simulation by asking whether an X originating at a defined source can reach a critical clock, reset, control signal, state machine or output under any behaviour allowed by the formal model. When it can, the resulting counterexample provides a path to debug rather than relying on a regression test to happen to stimulate and observe the condition. [1][2]

That makes X-propagation a particularly useful formal application during RTL bring-up, reset verification and targeted bug hunting.

Why an X is a verification problem, not a silicon logic level

SystemVerilog supports four-state logic: 0, 1, X and Z. The language semantics are defined by IEEE 1800. [3] For most ordinary synthesised digital logic, however, an internal hardware node eventually resolves electrically to a value interpreted as zero or one. An RTL X therefore represents uncertainty in the model rather than a third functional Boolean value in the fabricated circuit.

That distinction creates two familiar verification effects.

Consider control logic driven by a selector that is unknown immediately after reset. If the two possible hardware values lead down different branches, a simulator must represent that situation somehow. Standard language semantics can sometimes choose behaviour that appears deterministic even though the fabricated circuit could legitimately behave differently depending on the physical value assumed by the uninitialised state.This is why simply asking whether the waveform contains an X is not enough.

The better engineering question is:

Can uncertainty at this source influence behaviour that the specification requires to be deterministic?

Why reset and initialisation are common X-propagation hotspots

Reset logic defines part of the starting contract between the design and its environment. That contract becomes risky when verification silently assumes more initialisation than the RTL or hardware actually guarantees.

Common sources include:

• Registers that intentionally or accidentally have no reset
• Partially reset state machines
• Reset deassertion before dependent state has become valid
• Memories or arrays read before valid data has been written
• Control fields that are only initialised later by firmware
• Out-of-range array accesses
• Undriven or incompletely connected signals
• Power-gated state that becomes unknown during power-down or wake-up

Not every non-resettable register is a defect. Resetting every datapath register can be unnecessary or undesirable. A register may safely power up to either value if downstream logic cannot consume it until a valid indication is asserted.

The verification requirement is therefore not:

“Every register must have a reset.”

It is:

“No uncontrolled initial state may influence externally meaningful or safety-, security- or function-critical behaviour before that state becomes valid.”

A published Broadcom DVCon methodology provides a useful real example. Formal reset analysis found four flip-flops that could remain unknown during the first cycle after reset deassertion. One affected a state-machine decision. Standard RTL behaviour masked the problem through X-optimism, while formal X-propagation generated failing checks and a counterexample exposing the path. [1]

That is precisely the type of problem conventional reset-directed testing can struggle to expose reliably.

What formal X-propagation analysis actually asks

Formal X-propagation applications differ in implementation, but the central engineering model can be understood as a source-to-target reachability problem.

First, define or identify possible X sources. These might include:

• Non-reset registers
• Potentially unknown inputs
• Uninitialised memory state
• Deliberately modelled X-generating conditions
• Structural RTL defects
• Low-power state transitions

Then identify targets whose uncertainty matters, such as:

• Clocks
• Reset signals
• FSM state or next-state logic
• Mux selectors
• Enables
• Privilege or security controls
• Protocol-valid signals
• Architecturally visible outputs

The formal engine then evaluates whether uncertainty from the selected source can reach a target under the permitted input sequences, state transitions and constraints. Cadence describes this type of application as automatically checking sources and conditions that lead to unwanted X values and analysing clocks, resets, control/data structures and outputs. Synopsys describes formal X-propagation verification as checking unknown-value propagation and tracing a failed property back towards its X source. Siemens similarly provides an automated formal Check X application for RTL. [2][4][5]

The important word is permitted.

A formal result is only as meaningful as the model around it: reset assumptions, clock definitions, input constraints, source selection, abstraction and proof scope all affect what the engine is allowed to explore. That is why engineers developing this capability need more than a push-button understanding of an individual app. Alpinum’s practical formal verification training for hardware engineers covers the surrounding skills of constraints, proof analysis, debug, formal metrics and formal applications, including X-propagation.

A practical source-to-target workflow for X-state bugs

A useful X-propagation methodology can be organised into seven steps.

1. Define the reset and initial-state contract

Start by writing down what the design is actually guaranteed to know after reset.

1. Which registers are reset? 
2. Which are deliberately not reset? 
3. When do memories become valid? 
4. Must firmware configure anything before normal operation begins?
5. Can inputs change while reset is being removed?

This prevents the formal environment from assuming a cleaner start-up condition than the hardware receives.

2. Inventory potential X sources

Use RTL review, lint, structural/formal applications and reset analysis to locate candidate sources.

Do not immediately treat every candidate as a design bug. Classify each one as:

• Unintended
• Intentionally uninitialised but safely contained
• Environment dependent
• Low-power related
• Requiring further proof

This source-first approach is important because formal capacity is not unlimited. The Broadcom methodology found that identifying sources and choosing an appropriate analysis scope could be more effective than immediately applying X-propagation to an entire large IP. [1]

3. Eliminate obvious structural defects first

If the source is caused by an out-of-range index, undriven signal, incomplete assignment or accidental reset omission, fix the structural problem before spending proof capacity exploring its propagation.

This is an important distinction between source detection and behavioural propagation analysis. A structural checker might tell you that a register can be uninitialised. Formal X-propagation then asks whether that fact can matter somewhere important. The AHAA formal-verification framework provides a useful way to position this work: some techniques prevent defects, some hunt for them, some prove their absence, and others help analyse an already observed problem.

4. Select high-consequence targets

Do not start by proving that every datapath bit in the design is never X.

Prioritise points where uncertainty changes control or architectural behaviour:

This risk-based target selection makes the result more actionable and reduces unnecessary formal scope.

5. Run formal at the smallest useful scope

A common mistake is to start at full-SoC level simply because the eventual product is a SoC.Formal engines must reason over the reachable state space represented by the chosen cone and environment. Wider scope, more state and loose constraints can prevent convergence.A smaller block around the known X source and its meaningful destinations often produces a more useful answer.

The principle is the same as broader formal-verification adoption strategy select problems whose structure fits formal rather than treating formal as one monolithic replacement for the rest of verification.

6. Debug the counterexample as an engineering path

When a check fails, do not stop at “X reached output Y”.

Trace:

source → activation condition → propagation path → first critical consumer → architectural effect

For reset-related failures, pay particular attention to the first few cycles after reset removal. Ask whether the X is present before a valid qualifier, whether the affected branch can alter state, and whether later initialisation occurs too late to prevent the incorrect decision.This converts a waveform symptom into a design-intent question.

7. Verify the fix in more than one way

After correcting the RTL or legal operating constraint:

1. Rerun the formal check
2. Make sure the formerly failing path is no longer reachable
3. Confirm that the fix has not introduced an over-constraint
4. Exercise the relevant scenario in X-aware simulation where practical
5. Record any bounded or unresolved results in the verification plan

This last point matters. Verification planning should capture what has actually been proved, not merely that the tool was run. Alpinum’s guide to verification planning and coverage closure discusses the wider role of measurable evidence in sign-off.

A diagnostic matrix for RTL X-propagation

The following matrix can help teams choose the next verification action rather than treating every X symptom in the same way.

Formal X-propagation versus simulation and structural checks

The techniques are complementary rather than interchangeable.

The Broadcom study reached a similar methodological conclusion: source analysis, formal X-propagation and simulator X-propagation were most useful as complementary techniques rather than alternatives. Its whole-IP experiment also demonstrates an important warning: bounded formal results did not establish absence of a known bug. [1]

Therefore:

No reported failure is not the same as a proof that no X-propagation bug exists.

The proof status matters.

Reset and initial-state modelling traps

Assuming reset too strongly

An assumption that reset always arrives in one ideal sequence can exclude the transition that exposes the bug. Every assumption should be traceable to a real architectural or environmental guarantee.

Treating arbitrary initial state as equivalent to reset

Formal tools can deliberately start state elements from broad or arbitrary values. That can be powerful for bug hunting, but it changes the proof problem. Synopsys notes that allowing an unknown/arbitrary starting state can reveal failures quickly, but can also create spurious results if properties are not designed appropriately. [6]

A proof beginning from any theoretical state and a proof beginning after the legal reset sequence answer different questions.

Constraining away post-reset behaviour

If an input is constrained to remain idle until all internal state is already valid, the environment may become cleaner than the real system. This is one of the most dangerous formal mistakes because it can convert a real design failure into a green property.

Resetting everything simply to eliminate Xs

An X report is evidence to investigate, not an automatic instruction to add a reset. Some datapath or storage state can be safely uninitialised if the architecture prevents its consumption until valid. Adding reset merely to silence an analysis can increase reset distribution, implementation cost and complexity without addressing the intended behaviour.

Prove containment where containment is the design intent.

Low-power RTL makes the X problem more dynamic

Power gating adds another source of unknown state. When a block is powered down, retained and non-retained state behave differently. Isolation must prevent powered-down logic from corrupting active domains, and restored logic must not be consumed before the required state is valid.

Synopsys describes X-propagation analysis as useful alongside low-power simulation for investigating power-state transitions and distinguishing logical X sources from power-related ones. It also highlights isolation, retention, power switches and level shifting as relevant parts of the wider low-power verification problem. [7]

Formal X analysis can therefore provide useful evidence around control paths during wake-up, but it does not replace UPF consistency checks, isolation verification, power-aware simulation or a complete low-power verification methodology.

Common mistakes when using formal X-propagation

1. Treating every X as a defect

The presence of an unknown is less important than whether it can influence specified behaviour.

2. Forcing Xs to known values to keep regressions clean

Forcing a problematic source to zero may remove the symptom while also removing the behaviour verification should investigate.

3. Starting with the entire SoC

Large scope can turn a focused bug-hunting problem into a convergence problem. Start from validated sources and high-value targets.

4. Calling a bounded result a proof

A bounded result means the engine has established the property only within the explored depth or conditions. It is not equivalent to an unbounded proof.

5. Accepting constraints without challenge

Over-constraint can remove precisely the sequence required to expose the bug.

6. Confusing X analysis with CDC or metastability analysis

An X can be used in some simulation models to represent uncertainty around asynchronous behaviour, but X-propagation analysis is not a replacement for clock-domain crossing or reset-domain crossing verification.

7. Debugging only the destination

The output that becomes X may be several stages away from the actual error. Fixing a downstream mask can leave the original initialisation or control defect in place.

Where SystemVerilog Assertions fit

Some commercial formal X-propagation applications generate their own checks and do not require engineers to write an SVA for every source-to-target path. Cadence, for example, explicitly describes its XPROP application as automating the checks. [2]

That does not make assertion and formal-modelling skills irrelevant.

Once an X issue points to a behavioural requirement, engineers often need to express the real intent:

• A state must be legal after reset
• An output must not become valid before state is initialised
• A write enable must never depend on unknown control
• A retained value must be restored before it is consumed
• A qualifier must prevent uninitialised data becoming observable

Those are specification properties rather than generic X checks.

Engineers who need stronger SVA foundations can also use Alpinum’s SystemVerilog Training as an adjacent prerequisite resource.

Where X-propagation belongs in a verification strategy

X-propagation analysis is particularly valuable when a design contains:

• Complex reset sequencing
• Intentionally non-reset state
• Control-heavy FSMs
• Firmware-dependent initialisation
• Power gating or retention
• Third-party RTL with uncertain reset assumptions
• High-consequence safety or security control paths
• Repeated gate-level or silicon issues associated with initial state

It should normally be introduced before final sign-off, when the RTL and reset architecture can still be changed economically. It also fits naturally into a layered formal strategy. The AHAA model treats formal as a collection of applications rather than one single technique. X-propagation is one bug-hunting application. Property verification, reachability, security analysis and other formal techniques answer different questions.

For security-sensitive control, for example, the relevant next question may be whether untrusted information can influence a protected asset rather than whether a generic X can propagate. That is a different intent addressed in Alpinum’s guide to formal security verification for SoC design.

Conclusion: prove whether uncertainty can matter

X-propagation is most useful when it changes the engineering question from:

“Why is there an X in this waveform?”

to:

“Can this uncertain state reach behaviour that must be deterministic?”

Formal verification is well suited to the second question because it can explore source-to-target behaviour beyond the scenarios selected by a simulation regression. But the result is only defensible when reset modelling, constraints, proof scope and proof status are equally well understood.

A robust RTL flow therefore combines:

source identification → reset analysis → structural checking → targeted formal X-propagation → counterexample debug → X-aware simulation → documented sign-off evidence.

For engineers who want to develop those skills in a structured practical setting, Alpinum’s Formal Verification Training for Hardware and Software covers property writing, constraints, proof analysis, debug, metrics, formal applications including X-propagation, and the use of formal alongside simulation.

References used in this article

[1] S. Zhao, S. Yan and Y. Feng, “Practical Approach Using a Formal App to Detect X-Optimism-Related RTL Bugs,[Online]. Available: https://dvcon-proceedings.org/wp-content/uploads/practical-approach-using-a-formal-app-to-detect-x-optimism-related-rtl-bugs.pdf

[2] Cadence Design Systems, “Jasper X-Propagation Verification App.[Online]. Available: https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-verification-platform/jaspergold-x-propagation-verification-app.html

[3] IEEE, “IEEE Std 1800-2023 — SystemVerilog. [Online]. Available: https://standards.ieee.org/ieee/1800/7743/

[4] Synopsys, “VC Formal — Formal X-Propagation Verification.  [Online]. Available: https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html

[5] Siemens EDA, “Questa Check X.  [Online]. Available: https://www.siemens.com/en-us/products/ic/questa-one/formal-verification/check-x/

[6] Synopsys, “Managing Initial State in Formal Verification for Optimal Results. [Online]. Available: https://www.synopsys.com/blogs/chip-design/managing-initial-state-formal-verification.html

[7] Synopsys, “Running X-Propagation with Low Power Simulation. [Online]. Available: https://www.synopsys.com/blogs/chip-design/running-x-prop-with-low-power-simulation.html

FAQS