Technical Papers

Wireless

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.

Networking

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.

CPU / GPU / AI

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.

Video

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 managable 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

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.)