Verification Academy

Search form

My Account Menu

  • Register
  • Log In
  • Topics
  • Courses
  • Forums
  • Patterns Library
  • Cookbooks
  • Events
  • More
  • All Topics
    The Verification Academy offers users multiple entry points to find the information they need. One of these entry points is through Topic collections. These topics are industry standards that all design and verification engineers should recognize. While we continue to add new topics, users are encourage to further refine collection information to meet their specific interests.
    • Languages & Standards

      • Portable Test and Stimulus
      • Functional Safety
      • Design & Verification Languages
    • Methodologies

      • UVM - Universal Verification Methodology
      • UVM Framework
      • UVM Connect
      • FPGA Verification
      • Coverage
    • Techniques & Tools

      • Verification IP
      • Simulation-Based Techniques
      • Planning, Measurement, and Analysis
      • Formal-Based Techniques
      • Debug
      • Clock-Domain Crossing
      • Acceleration
  • All Courses
    The Verification Academy is organized into a collection of free online courses, focusing on various key aspects of advanced functional verification. Each course consists of multiple sessions—allowing the participant to pick and choose specific topics of interest, as well as revisit any specific topics for future reference. After completing a specific course, the participant should be armed with enough knowledge to then understand the necessary steps required for maturing their own organization’s skills and infrastructure on the specific topic of interest. The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization’s processes so that you can then reap the benefits that advanced functional verification offers.
    • Universal Verification Methodology (UVM)

      • Advanced UVM
      • Basic UVM
      • Introduction to UVM
      • UVM Connect
      • UVM Debug
      • UVMF - One Bite at a Time
    • Featured Courses

      • Introduction to ISO 26262
      • Introduction to DO-254
      • Clock-Domain Crossing Verification
      • Portable Stimulus Basics
      • Power Aware CDC Verification
      • Power Aware Verification
      • SystemVerilog OOP for UVM Verification
    • Additional Courses

      • Assertion-Based Verification
      • An Introduction to Unit Testing with SVUnit
      • Evolving FPGA Verification Capabilities
      • Metrics in SoC Verification
      • SystemVerilog Testbench Acceleration
      • Testbench Co-Emulation: SystemC & TLM-2.0
      • Verification Planning and Management
      • VHDL-2008 Why It Matters
    • Formal-Based Techniques

      • Formal Assertion-Based Verification
      • Formal-Based Technology: Automatic Formal Solutions
      • Formal Coverage
      • Getting Started with Formal-Based Technology
      • Handling Inconclusive Assertions in Formal Verification
      • Sequential Logic Equivalence Checking
    • Analog/Mixed Signal

      • AMS Design Configuration Schemes
      • Improve AMS Verification Performance
      • Improve AMS Verification Quality
  • All Forum Topics
    The Verification Community is eager to answer your UVM, SystemVerilog and Coverage related questions. We encourage you to take an active role in the Forums by answering and commenting to any questions that you are able to.
    • UVM Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • UVM Forum
    • SystemVerilog Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • SystemVerilog Forum
    • Coverage Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • Coverage Forum
    • Additional Forums

      • Announcements
      • Downloads
      • OVM Forum
  • Patterns Library
    The Verification Academy Patterns Library contains a collection of solutions to many of today's verification problems. The patterns contained in the library span across the entire domain of verification (i.e., from specification to methodology to implementation—and across multiple verification engines such as formal, simulation, and emulation).
    • Implementation Patterns

      • Environment Patterns
      • Stimulus Patterns
      • Analysis Patterns
      • All Implementation Patterns
    • Specification Patterns

      • Occurrence Property Patterns
      • Order Property Patterns
      • All Specification Patterns
    • Pattern Resources

      • Start Here - Patterns Library Overview
      • Whitepaper - Taking Reuse to the Next Level
      • Verification Horizons - The Verification Academy Patterns Library
      • Contribute a Pattern to the Library
  • All Cookbooks
    Find all the methodology you need in this comprehensive and vast collection. The UVM and Coverage Cookbooks contain dozens of informative, executable articles covering all aspects of UVM and Coverage.
    • UVM Cookbook

      • UVM Basics
      • Testbench Architecture
      • DUT-Testbench Connections
      • Configuring a Test Environment
      • Analysis Components & Techniques
      • End Of Test Mechanisms
      • Sequences
      • The UVM Messaging System
      • Other Stimulus Techniques
      • Register Abstraction Layer
      • Testbench Acceleration through Co-Emulation
      • Debug of SV and UVM
      • UVM Connect - SV-SystemC interoperability
      • UVM Versions and Compatibility
      • UVM Cookbook
    • Coding Guidelines & Deployment

      • Code Examples
      • UVM Verification Component
      • Package/Organization
      • Questa/Compiling UVM
      • SystemVerilog Guidelines
      • SystemVerilog Performance Guidelines
      • UVM Guidelines
      • UVM Performance Guidelines
    • Coverage Cookbook

      • Introduction
      • What is Coverage?
      • Kinds of Coverage
      • Specification to Testplan
      • Testplan to Functional Coverage
      • Bus Protocol Coverage
      • Block Level Coverage
      • Datapath Coverage
      • SoC Coverage Example
      • Requirements Writing Guidelines
      • Coverage Cookbook
  • All Events
    No one argues that the challenges of verification are growing exponentially. What is needed to meet these challenges are tools, methodologies and processes that can help you transform your verification environment. These recorded seminars from Verification Academy trainers and users provide examples for adoption of new technologies and how to evolve your verification process.
    • Upcoming & Featured Events

      • Low Power Verification - 4/29
      • Fault Campaign for Mixed-Signal - 5/4
      • User2User - 5/26
      • Webinar Calendar
    • On-Demand Webinars

      • CDC+RDC Analysis
      • Basic Abstraction Techniques
      • Safety Analysis Techniques
      • QVIP Workflow and Debug for PCIe
      • Writing a Proxy-driven Testbench
      • Achieving High Defect Coverage
      • Visualizer Features
      • All On-Demand Webinars
    • Recording Archive

      • Siemens EDA 2021 Functional Verification Webinar Series
      • Improving Your SystemVerilog & UVM Skills
      • Should I Kill My Formal Run?
      • Visualizer Debug Environment
      • Industry Data & Surveys
      • All Recordings
    • Conferences

      • DVCon 2021
      • DVCon 2020
      • DAC 2019
      • All Conferences
    • Mentor Learning Center

      • SystemVerilog Fundamentals
      • SystemVerilog UVM
      • View all Learning Paths
  • About Verification Academy
    The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization's processes so that you can then reap the benefits that advanced functional verification offers.
    • Blog & News

      • Verification Horizons Blog
      • Academy News
      • Academy Newsletter
      • Technical Resources
    • Verification Horizons Publication

      • Verification Horizons - March 2021
      • Verification Horizons - November 2020
      • Verification Horizons - July 2020
      • Issue Archive
    • About Us

      • Verification Academy Overview
      • Subject Matter Experts
      • Contact Us
    • Training

      • Questa Basic
      • Questa Advanced
      • Mastering Questa
  • Home
  • Verification Horizons
  • June 2013
  • Confidence in the Face of the Unknown: X-state Verification

Confidence in the Face of the Unknown: X-state Verification

Verification Horizons - Tom Fitzpatrick, Editor

 X-state Verification 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:

  1. Activation of an explicit X-state assignment (that was likely intended as a synthesis don't care)
  2. Bus driver value conflicts
  3. Out of range indexing
  4. 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

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

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

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:

  1. Automatic formal analysis produces results showing sources of X-states and X-propagation assertions
  2. 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

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

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

  1. Lionel Bening, "A Two-State Methodology for RTL Logic Simulation," Proc. 36th Design Automation Conf., June 1999.
  2. Lionel Bening and Harry Foster, Principles of Verifiable RTL Design, Kluwer Academic Publishers, May 2001.
  3. 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
  4. Roger Sabbagh, "The Top Five Formal Verification Applications", Verification Horizons, October 2012
  5. Kaowen Liu, et al., "Using Formal Techniques to Verify System on Chip Reset Schemes", Proc. DVCon 2013, February 2013

Back to Top

Table of Contents

Verification Horizons Articles:

  • An Up-sized DAC Issue Takes the Stage

  • Interviewing a Verification Engineer

  • Maximum Productivity with Verification IP

  • Power Up Hardware/Software Verification Productivity

  • Non-invasive Software Verification using Vista Virtual Platforms

  • QVM: Enabling Organized, Predictable, and Faster Verification Closure

  • Verifying High Speed Peripheral IPs

  • Confidence in the Face of the Unknown: X-state Verification

  • Making it Easy to Deploy the UVM

  • NoC Generic Scoreboard VIP

  • Flexible UVM Components: Configuring Bus Functional Models

  • Monitors, Monitors Everywhere – Who Is Monitoring the Monitors?

  • The Need for Speed: Understanding Design Factors that Make Multi-core Parallel Simulations Efficient

Siemens Digital Industries Software

Siemens Digital Industries Software

##TodayMeetsTomorrow

Solutions

  • Cloud
  • Mendix
  • Siemens EDA
  • MindSphere
  • Siemens PLM
  • View all portfolio

Explore

  • Digital Journeys
  • Community
  • Blog
  • Online Store

Siemens

  • About Us
  • Careers
  • Events
  • News and Press
  • Newsletter
  • Customer Stories

Contact Us

USA:

phone-office +1 800 547 3000

See our Worldwide Directory

  • Contact Us
  • Support Center
  • Give us Feedback
©2021 Siemens Digital Industries Software. All Rights Reserved.
Terms of Use Privacy Cookie Policy