Technical Papers


Architectural Formal Verification of System-Level Deadlocks

Presented by Qualcomm

Formal verification applications have been evolving over the past few decades to address problems at increasingly higher levels of hardware design complexity. The latest step in this evolution has been the introduction of architectural formal verification methodologies to target system-level requirements. This paper describes our architectural formal verification process, including the development and use of architectural models, and we present a case study of how this method was applied to verify the absence of deadlocks in an industrial design.


End-to-End Formal using Abstractions to Maximize Coverage

Presented by Cisco

The use of abstraction models is key to overcoming complexity barriers in applying formal verification.. In this paper, we show how simulation-like coverage metrics can be used to determine the completeness of a formal verification setup, for a real-world design with a large state space, that needed abstractions for end-to-end proofs.

Formal Verification of Software Configurable Silicon for SDN

Presented by Cavium (Marvell)

The configurability of multi-terabit Software Defined Networking devices ushers in a new level of challenge in the verification process. The number of combinations of configuration settings exceeds the practical limits of traditional verification methods. This paper describes how formal verification methodology was used to address this challenge on the Cavium XPliant® Ethernet Switch designs.

Deploying Model Checking for Bypass Verification (BEST PAPER AWARD)

Presented by Cisco

Bypass logic in used to achieve performance in deeply pipelined designs, but comes at a significant increase in verification complexity. This paper describes how we applied model checking to establish the correctness of the bypass case, and found corner case bugs that are almost impossible to find with simulation.

How Formal Methodology Shrank the Verification Schedule of a Complex Statistics Block by 6x

Presented by Cisco

To insure high quality of service, today’s routers need to record and react to numerous statistics in real time, across all the routing paths. Architectural features needed to support the throughput requirements risked creating numerous corner cases. This presentation summarizes how an 18-month simulation-based effort was shrunk down into only 3 months using formal verification.


Detecting Circular Dependencies in Forward Progress Checkers

Presented by NVIDIA

Forward progress checkers are often implemented with embedded stall conditions, which are conceptually equivalent to implicit constraints. These constraints cannot be verified using traditional methods, such as assume-guarantee, and hence they introduce the risk of missing deadlock bugs due to circularity in the proofs. In this paper, we present a method for detecting circular dependencies in this style of forward progress checker and share results of applying this method to the blocks of a GPU system design.

Finding the Last Bug in a CNN DMA Unit

Presented by Synopsys

Functional formal sign-off of design blocks provides the benefit of finding all bugs, no matter how resistant they are to discovery through traditional methods. The Direct Memory Access (DMA) unit of a Convolutional Neural Network (CNN) is a design that has very long memory volume transport latencies, which is a characteristic that would conventionally cause it to be considered incompatible with formal verification. However, in this paper, we present a repeatable process that enables the successful application of formal sign-off to such designs. We will show how we were able to find extreme corner case bugs and have confidence that we had found the last bug.

Using Formal Tools to Verify Datapath Designs During Various Phases of Processor Development

Presented by AMD

It is a challenging problem to formally verify mathematical datapath designs. Such designs, by nature, do not lend themselves well to be verified via traditional model checking algorithms. However, formal transactional equivalence checking with a “golden” reference model can be used successfully to verify datapath designs. In this paper, we describe how we used HECTOR – a C-vs-RTL transactional equivalence checking tool from Synopsys – to formally establish the correctness of a multiplier design for an X86 processor core. We also used the Synopsys VC Formal tool to prove correctness of a complex divider design. The transactional equivalence checking was repeated several times as the designs went through changes to satisfy power and performance requirements. Due to the large complexity in the designs, we pushed the limits and had deployed various recipes and techniques, including transitivity and assume-guarantee.

Formal Verification of a Public-Domain DDR2 Controller Design

Using the Sun OpenSPARC DDR2 Memory Controller design that has been in the open-source public domain, this paper removes much of the mystery in a successful application of end-to-end formal verification on a memory controller design.


Creative Formal Techniques to Verify PCache

Presented by Broadcom

Coloring is a very powerful formal technique to verify data transport designs. It adds minimum number of flops to the formal testbench, making formal complexity manageable by formal tools. PCache is a data transport design and an ideal fit for formal verification. However, conventional coloring technique cannot be readily used as PCache allows drop data based on certain rules. To formally verify PCache, we came up with creative ideas to enhance the conventional coloring technique, without adding complexity to the formal testbench. We found 12 bugs using the technique and achieved formal sign-off on Pcache.

PCIe / Ethernet

Formal Verification for PCI Express RTL Designs

PCI Express is a classical example of a design that can result in severe complexity challenges in formally verifying end-to-end properties. Yet, data-transport designs like this can be successfully verified using creative abstraction methods. This presentation discusses general strategies for verifying a PCI Express design.

SoC – All Domains

Discovering Deadlocks in a Memory Controller IP

Presented by u-blox

The risk of deadlocks is one of the areas that is not well addressed by dynamic testing. Simulation does not provide the tools to target deadlocks directly, so finding deadlock scenarios generally happens by chance. On the other hand, formal verification is particularly well suited to verifying a wide range of forward progress properties of designs, such as absence of deadlock, live-lock, and starvation. In this paper, we present a formal verification methodology that has been shown to predictably discover deadlock in RTL designs. The methodology is applicable in the early phases of IP development and design integration. We share results from the application of the method on an industrial memory controller IP.

Guidelines for Creating a Formal Verification Testplan (BEST PAPER AWARD)

This paper proposes a systematic set of guidelines for creating an effective formal verification testplan, which consists of an English list of comprehensive requirements that capture the desired functionality of the blocks that are to be verified.

The Process and Proof for Formal Sign-Off – A Live Case Study

With the advances in formal technology and the introduction of Formal Sign-off Methodology in recent years, it has become possible to create a formal testbench that can find all bugs in a design. However, this is a very new concept that most design and verification teams do not know well enough to adopt and leverage for sign-off. The paper explains in detail the process to achieve Formal Sign-off, focusing on End-to-End checkers, constraints, complexity and formal coverage. In addition, we present a live case study as proof that Formal Sign-off is possible.

Sign-off with Bounded Formal Verification Proofs (2nd BEST PAPER AWARD)

Presented by Samsung

Inconclusive formal verification results or bounded proofs have been hindering the adoption of formal verification. This paper describes a formal sign-off methodology in presence of bounded proofs. With an understanding of the DUT and a systematic analytical approach, we can qualify bounded proofs and use Abstraction Models to achieve formal sign-off.

Formal Verification of a Highly Configurable DDR Controller IP

Presented by Synopsys

In this paper, we describe the formal verification methodology used for the AMBA AXI Port Interface (XPI) controller of the Synopsys DesignWare Cores DDR Memory Controller. The controller is feature-rich and the XPI is a highly configurable design, which varies with both hardware and software configuration parameter settings. This creates a formidable challenge for traditional verification methods as there are many combinations of settings resulting in long simulation cycles to reach the coverage objectives. Contrast this with formal verification, which uses mathematical algorithms to efficiently test design behaviors for all possible stimulus and configurations. We will describe the formal verification flow including configurable formal testbench implementation and formal coverage closure.

Compositional Reasoning Gotchas in Practice

Presented by Ikanos (Qualcomm) / NVIDIA

Model checking has become a formal sign-off requirement in the verification plans of many hardware designs. For design sizes encountered in practice, compositional assumeguarantee reasoning is often necessary to achieve satisfactory results. However, many pitfalls exist that can create unsound or unexpected results for users of commercial model checking tools. Users need to watch out for circularity in properties, for dead-ends getting trimmed by tools, as well as understand the differences in proof composition for liveness and safety properties. We present many real design examples to illustrate these points, as well as describe our experiences with compositional reasoning in practice.

Liveness vs Safety – A Practical Viewpoint

Presented by Chelsio / NVIDIA

Within the formal verification community, choosing between liveness and safety approaches has long been a subject of debate. This paper applies both approaches to a common design in the networking industry, a Deficit Weighted Round Robin (DWRR) arbiter. It then presents the tradeoffs we encountered while applying both approaches and also describes how we overcame state space explosion. We also describe two real post-silicon design bugs that we found, which were missed by all simulation methods.

Using Coverage to Deploy Formal in a Simulation World

Formal verification can complement or replace simulation effort for selected hardware designs. In this paper we discuss how formal verification can be deployed using simulation-based coverage in a simulation-based verification schedule.

Modeling Xs in Behavioral Models of Hard IPs

Presented by Cypress / NVIDIA

Behavior models of hard IPs are often used to replace traditional SPICE models to reduce simulation time. However X-modeling is prone to simulation race conditions and is hard to verify which could lead to missing bugs in SoC integration. We present an assertion-based approach of verifying X-modeling of a behavioral model which handles simulation race conditions and avoids false positives and negatives. Our approach is the first solution that can be used by developers of behavioral models to systematically detect missing X-assignment bugs.

Who Verifies Your Third-Party Design IP?

This July 2006 issue contains an article that argues that third-party design IP must be accompanied by replayable verification IP, that proves the correctness of the design through end-to-end checks. (Go to page 3 of the issue to find the article.)

Covering the Last Mile in SoC-Level Deadlock Verification

Verifying the absence of System-on-Chip (SoC) deadlocks when integrating a wide variety of Intellectual Property (IP) cores and interconnect fabrics from various internal and third-party sources is a daunting challenge. Current solutions are typically composed of a combination of technologies such as full-chip simulation, emulation and hardware prototyping. However, deadlock scenarios often occur in rare cases that involve several preconditions occurring in sequence and with specific timing. Consequently, deadlock bugs may only be triggered in extreme corner-case conditions, which are resistant to discovery by traditional methods. In this paper, we present a formal verification solution that exploits the exhaustive nature of formal analysis to overcome this resistance and deliver the confidence required for sign-off.