Three Steps To Complete Reset Behavior Verification

By Chris Kwok, Priya Viswanathan, and Ping Yeung

Reset architectures are notoriously complex and difficult to verify. Today’s SoCs contain highly complex reset distributions and synchronization circuitry. Often, reset trees can be larger than clock trees and have many of the same potential issues.

Verifying that a design can be correctly reset under all modes of operation presents significant challenges. Yet, failure to catch reset related bugs cause costly, late-stage design changes and, in the worst case, silicon respins and time-to-market delays. Typically these types of bugs are of a very serious nature, rendering the chip completely unusable.

Many of the issues are hard to catch bugs that cannot be easily debugged with simulation or traditional verification techniques. Simulation cannot achieve complete test coverage and gate-level simulation is run too late in the design cycle.

To overcome these deficiencies and to ensure correct reset tree implementation and proper reset usage, a comprehensive three-stage verification solution is required that consists of:

• Static analysis of the design structure
• RTL simulation with X-propagation
• Formal analysis

This article describes this three-part methodology for solving reset verification challenges. Each of the three steps has its strengths and weaknesses. As they complement each other in various ways, a complete solution needs to involve all three.

Automated reset verification

1. Static Analysis
Determining the reset tree (Figure 1) can be done by performing static analysis on the RTL using an automated formal verification tool. Because static analysis only requires RTL, it can be performed without having to create testbench stimulus or assertions, and it eliminates the need to wait for gate-level simulations.

Figure 1: Typical reset tree topology.

A reset domain is characterized by the following attributes:

• Type: synchronous or asynchronous
• Polarity: active low or active high
• Value: set for 1 and reset for 0
• The top resetting signal

First the resets are identified through synthesis. Then they are classified as either synchronous or asynchronous resets, and whether they are active high or active low resets. Top reset signals are recognized in the design by identifying the structural templates for synchronous and asynchronous reset pins of a register and their respective polarities.

Once the reset tree is built, it can be annotated with multiple layers of design information, including clock, power, and delay levels. The generation of the detailed reset tree enables structural checks on the reset architecture. Results of the static analysis vary from simple informative checks to complex functional checks.

Some examples of informative checks are:

• Resets that are used as active low and active high in the design
• Resets that are used asynchronously and synchronously
• Conflicts in usage of resets between specification and usage
• Resets used as data

The static analysis also performs functional checking for reset issues. Some examples are:

• Asynchronous reset domain crossings
• Reset synchronizer structures and their reconvergence
• Reset delay protocols
• Glitch detection

Most modern chips employ multiple clock domains. Metastability in a design due to asynchronous clock domain crossings is a well-known issue. However, even if the data path is in the same clock domain, if the reset domain of the source register is different from that of the destination register, the asynchronous crossing path can still cause metastability at the destination register. Correctly implementing these crossings involves understanding the use of reset domains and their interaction with clock domains. Figure 2 shows a circuit which could have such metastability problems.

Figure 2: A circuit with potential metastability problems.

In a complex SoC design with multiple reset sources and a large number of registers, there could be millions of reset related violations. A sophisticated debug methodology and environment is essential to help users manage the violations, as well as understand and debug the real issues.

The disadvantage of static analysis is that, in many cases, it can show only that there are potential problems. To show that the problem actually exists in the design, we need to rely on RTL simulation or a model checking formal engine. This requires users to write SVA assertions. In some cases, tools can also generate the assertions to be used by RTL simulation and formal verification.

2. RTL Simulation with X-Propagation
RTL simulation with silicon-accurate X-propagation semantics can be used to find issues related to uninitialized design elements, which cannot be found by static analysis. X-propagation addresses X-optimism by propagating X values forward in time. It involves if statements, case statements, and conditional assignments. For example, when a conditional expression has the value of X, an X-propagation enhanced simulator changes the language semantics to propagate X values. These values can be observed in simulation waveforms and in the downstream logic affected by the propagated X values.

If the Xs are not blocked or handled correctly in the design, the simulation could fail. In particular, the design’s silicon implementation could be subject to random failures that are completely missed by normal RTL simulation.

3. Formal Verification
Although simulation-based verification is capable of detecting many design bugs, it requires a proper testbench stimulus. Model checking technology can be used to supplement traditional simulation methods. For example, formal verification can be used to verify these reset tree properties:

• Connectivity of all sources of resets to their intended destinations
• X-pessimism and X-optimism
• Corruption of correctly reset storage elements with unknown logic values

Most of the reset problems resulted in X-states and eventually resulted in silicon bugs.

Conclusion
Reset architectures present hard to catch bugs that cannot be caught easily with simulation or traditional verification techniques. These complex issues require a full suite of methods involving static analysis, simulation, and formal analysis.

The Questa Reset Check App – based on CDC analysis technology – can be employed to automatically perform an exhaustive, bottom-up reset tree analysis, then automatically generate and prove assertions that cover numerous reset-specific structural checks.

For a description of the common reset problems themselves as well as results of using this three-part solution on real-world designs, please download the paper Addressing the Challenges of Reset Verification in SoC Designs.

For more on this topic, see A Specification-Driven Methodology for the Design and Verification of Reset Domain Crossing Logic to learn about a requirements-based approach for reset domain crossing design and verification.

Priya Viswanathan is a Staff Engineer at Mentor, A Siemens Business. She is currently a member of the Austemper functional safety verification R&D group. Prior to that, Viswanathan worked on the development of the Questa CDC and Questa Reset Check products. Viswanathan received an M.S. in Computer Engineering from San Jose State University.

Chris Kwok is a Principal Engineer at Mentor, A Siemens Business. Until recently, Kwok led the Questa CDC and Questa Reset Check R&D group. He is currently working on the Austemper functional safety verification tools. Kwok received an M.S. in Computer Science from UCLA.

Ping Yeung, Ph.D. is the Principal Engineer in the functional verification division of Mentor Graphics, a Siemens Business. He has over 20 years of application, marketing, and product development experience in the EDA industry, including positions at 0-In, Synopsys, and Mentor Graphics. He holds 9 patents in the CDC and formal verification areas.