June 7, 2010 -- Traditionally, simulation-based dynamic verification techniques — such as directed tests, constrained-random simulation, and hardware acceleration — have been the work horse of functional verification. As modern day SOC designs become more integrated, the only way to advance significantly beyond dynamic verification is to increase the adoption of static verification. Leading-edge design teams have been using static verification successfully for a long time. It has been used strategically by designers to improve design quality and to complement dynamic verification on coverage closure.
Static verification techniques help accelerate the discovery and diagnosis of design flaws during functional verification, reducing the time required to verify a design and simplifying the overall development cycle for complex SOC designs. In this article, we will summarize a variety of static verification techniques; including RTL lint, static RTL checks (which include low power structure verification and clock domain crossing verification), sequential formal checks, automatic formal applications, and assertion-based formal property verification.
As static analysis sees the RTL code and the synthesized representation of the design, it can naturally identify simulation and synthesis mismatches. By checking the synthesized representation of the design, it can highlight code segments that will cause synthesis to generate incorrect or inefficient logic. By analyzing the formal representation, it can identify potentially unreachable code and redundant functionality. All of this is important information, enabling designers to find better ways to rewrite the RTL code early in the design phase of the project.
Static analysis of gate-level netlists is also important. Synthesis and logic equivalence checking (LEC) have helped us move the majority of the design effect to the RTL. However, to design for test and design for power, many transformations are still performed on the gate-level netlist. Hence, it is still desirable to verify some specific functionality at the gate-level to ensure the transformations have been performed correctly and the functionality of the design has not been changed.
After a design has been fabricated, it is extremely difficult to debug any silicon related problems. Hence, anything that can be done up-front to prevent them will be extremely useful. Incrementally, based on the painful lessons learned debugging silicon failures, classes of static checks have been developed to look for these failure signatures at the RTL or gate-level. Two examples of this type of silicon failure are clock-domain crossing (CDC) metastability, and power domain isolation. Both of these cannot be verified efficiently with dynamic simulation. Instead, static verification can be performed to ensure design structures, such as synchronizers, are in place to safeguard against any metastability issues.
Five static verification technologies
1) RTL lint
RTL lint is a design and coding guideline checker. It checks HDL code for synthesizability, simulatability, testability, reusability, and RTL/ gate signoff. The rules capture years of experience. Besides helping to enforce some known good naming schemes, they are designed to explore design and coding deficiencies that impact simulation, synthesis, test, and performance. RTL lint enables design reuse with prepackaged guidelines , such as the Reuse Methodology Manual (RMM), and STARC. Some of the common RTL lint rules include:
- Un-synthesizable constructs.
- Unintentional latches.
- Unused declarations.
- Multiply driven and un-driven signals.
- Race conditions.
- Incorrect usage of blocking and non-blocking assignments.
- Incomplete assignments in sub-routines.
- Case statement style issues.
- Set and reset conflicts.
- Out-of-range indexing.
2) Static checks
Static checking tools perform a pseudo-synthesis of the design into structural elements, such as registers, latches, combinational logic, finite-state-machines, and RAM. Most static checks are performed on this structural netlist. Hence, static checks can recognize any deficient or incorrect coding style for synthesis and, at the same time, identify any simulation versus synthesis mismatch issues. As the checks are no longer constrained by the module boundaries, they can explore connectivity issues, fan-in, and fan-out (driver-reader) relationships within a design. However, it is important to realize that if part of the design is not synthesizable, it will be treated as a black box and static checks will not be performed. Some of the common static checks include:
- Combinational loops.
- Full and parallel case issues.
- Clock gating and usage issues.
- Bus conflicts and floating bus.
- Dead code or unreachable blocks.
- Unused input and un-driven output ports.
- Un-resettable registers.
- Dead-end states.
- Self-looping states.
- Unreachable states.
- Arithmetic overflow.
Two of the static checks getting a lot of attention for today’s designs are clock domain crossing checks  and low power structure checks .
3) Formal checks
Formal checks are performed on the formal netlist representation of a design. The formal representation incorporates the environmental constraints, the operational conditions, the design configurations, and the initialization sequence of the design. It represents how the design will operate clock cycle by cycle. Sequential design elements are represented in abstracted flow graphs; FSMs in state-transition graphs. Although formal checks have a lot of similarity with static checks, it does not focus only on structural connectivity, but also on functionality. The formal netlist allows the tool to calculate the possible values in the storage elements and nets of a design. As a result, it can foresee whether some scenarios are possible or not. For instance, if there are combinational loops in a design, formal checks can identify structural loops which are functionally impossible. This is useful as designers can focus on fixing the true combinational loops that actually can occur.
Most designs have dead code, unreachable blocks, and redundant logic. This is especially true for IP or reused blocks. They often have extra functionality that is not needed for the current design. If passive coverage metrics, such as line coverage, FSM coverage, or expression coverage, are part of the closure criteria, unused functionality will have negative impact on the coverage number. Formal checks can be used to identify these unreachable blocks and redundant logic up-front, hence excluding them from the coverage measurement.
Especially with dead code and FSM analysis, formal checks are more comprehensive. They can identify signals which will stick at particular values. As a result, they will lead to functionally redundant logic. For instance, a user may specify that two inputs of a design are mutually exclusive. Then, by analyzing the functionality of the design, formal checking can identify which parts of their fan-out are functionality unreachable. Some other related formal checks are:
- Functional combinational loops.
- Functional dead code.
- Unreachable functionality.
- Live and dead lock states.
- Unreachable states.
- Stuck at constant.
Other uses of formal checks are related to x-assignments, x-propagation, and x-termination . The goal is to eliminate pessimistic x-propagation as seen in simulation and to make sure an unknown or x-state is not generated or consumed unintentionally in the design. When an unknown state or an un-initialized state is sampled, the resultant value is unpredictable. Hence, it is also important to ensure that registers are initialized before they are used. Connecting a global reset to all the registers is ideal. However, due to routing congestion, it may not be always possible. The common formal checks related to X-state verification are:
- Reachable x-assignment.
- Unguarded x-termination.
- Un-initialized registers.
- Use of un-initialized values.
4) Automated formal applications
For some specific applications, formal verification can be applied to verify the structural correctness of a design. Similar to traditional formal property verification, assertions are used to capture the properties of the design. However, instead of being written manually, the assertions are generated automatically from their requirement specification. The verification process is completely streamlined. Here, we need to look at logic equivalence checking, timing constraint verification, and circuit property verification.
Logic equivalence checking (LEC) has been used extensively to perform RTL-to-gate level verification. It ensures that the gate-level netlist has implemented the RTL functionality correctly. To make sure the result is trustworthy, the assumptions used during the process need to be verified. FPV can help identify serious problems, such as conflicting assumptions and the violation of internal assumptions in library cells. Verifying functionality like these at the gate-level with simulation is extremely slow and it is impossible to cover all the possible scenarios. However, FPV will work well once the properties are derived from the gate-level netlist automatically.
After the synthesis process, static timing analysis (STA) has been used extensively to identify the critical paths and to ensure the gate-level netlist has met timing requirements. STA works well on single cycle paths; however, not all of them are real, functional paths. Some of them are false paths (FP). In addition, STA can easily be misled by multi-cycle paths (MCP), paths between asynchronous clock domains, and paths between ratio synchronous clock domains. Hence it is important to identify these exceptions as constraints for STA and to ensure these constraints are specified correctly. Assertions can be generated to capture these FPs, MCPs, and CDC paths automatically. Then, FPV can be used to verify the correctness of these constraints.
As it is extremely difficult to debug any silicon related problem, anything we can do up-front to prevent them from happening will be very beneficial. One goal is to make sure the design meets the "cycle-repeatable operation" (CRO) criterion . This means that the design can run a given test multiple times deterministically, with each run passing through the same internal states in the same order each time. In microprocessor designs, one of the requirements for CRO is to ensure one path is always selected in a pass transistor-based multiplexer. This is an easy property to capture in an assertion. Once it is done, FPV can be used to verify all of them in the design.
5) Formal property verification (FPV)
For design teams to adopt FPV successfully on a design, we recommend they deploy FPV first on verification hot spots . Verification hot spots are areas of concern within the design that are difficult to verify using traditional simulation-based methodologies. By focusing FPV on the hot spots, a design team can adopt FPV incrementally, side-by-side with their simulation-based methodology.
We recommend each design team to focus on the verification hot spots in four design areas:
- Resource control logic.
- Design interfaces.
- Finite state machines.
- Data integrity.
In addition, they can conduct an internal review to explore the unique hot spots in their designs. For formal property verification, design interfaces are popular verification hot spots among our customers. Interface verification using this approach has been employed successfully by a lot of our customers.
For verification purposes, we classify finite state machines (FSM) into two categories: interface FSMs and computational FSMs. Bus controllers and handshaking FSMs are examples of interface FSMs. Examples of computational FSMs are flow charts, data or control flow graphs. By capturing the properties of FSMs using assertions, we can identify them easily, exercise them completely and collect cross-product coverage information during the simulation process. When several FSMs are interacting with each other, it is important to ensure that they do not get "trapped" in a corner-case behavior. Formal verification can be applied to check this situation.
We also analyzed how the design teams added other assertions. Most of the teams spent significant effort on the resource control logic and data integrity hot spots. Assertions for resource control logic, such as arbiters, were easier to capture. Checkers from the assertion library were used extensively. Since most simulation environments did not stress test the resource control logic sufficiently, FPV did well and found a number of corner-case bugs. On the other hand, the assertions required to capture data integrity properties were complex, especially when data was reformatted, repackaged, or dropped intentionally. However, once these complex assertions were in place, they could be verified with various methodologies. They also represented an essential part of the verification plans; so the effort was well spent. Importantly, some of the bugs found were both critical and obscure. None would have been found with simulation alone.
In this article, we discussed five prominent static verification methodologies that can be used to supplement dynamic verification. They allow verification to start early in the design cycle when designers are still working on the RTL code. Formal checks are unique in delivering both ease-of-use and accuracy. By automating the assertion creation process, we have helped deploy formal property verification to target specific verification applications. Finally, verification hot spots are tried and true sweet spots for FPV. With formal technology, these static verification methodologies can examine all the possible scenarios in the design and find bugs missed by traditional simulation techniques.
As we have experienced with our customers, strategic deployment of static verification methodologies has proven to be effective. Static verification helps improve verification efficiency and boost the overall quality of the design.
By Ping Yeung Ph.D.
Ping Yeung, a Mentor Graphics’ principal engineer, was part of the 0-In team that developed and introduced assertion-based verification (ABV) to the industry. He has over 16 years’ in application development, marketing, and product development experience in the EDA industry, including positions at 0-In, Synopsys, and Mentor Graphics. He holds 5 patents in CDC and formal verification.
 "Developing an Effective Methodology for Checking RTL," Mentor white paper.
 "Five Steps to Quality CDC Verification," Mentor white paper.
 "Advanced Verification of Low Power Designs," Mentor white paper.
 "Sources of Non-Determinism in Microprocessor," J. Golab, Freescale Semiconductor, DesignCon 2008.
 "The Dangers of Living with an X," ARM, Mike Turpin.
 "Applying Assertion-Based Formal Verification to Verification Hot Spots," Mentor white paper.
Go to the Mentor Graphics Corp. website to learn more.