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