Technical Papers

Technical Papers

Formal Verification of a Highly Configurable DDR Controller IP

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 …

Formal Verification of a Highly Configurable DDR Controller IPRead More »

Formal Verification of Software Configurable Silicon for SDN

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.

Architectural Formal Verification of System-Level Deadlocks

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 Formal Verification of System-Level DeadlocksRead More »

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

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 …

Using Formal Tools to Verify Datapath Designs During Various Phases of Processor DevelopmentRead More »

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 …

The Process and Proof for Formal Sign-Off – A Live Case StudyRead More »

Compositional Reasoning Gotchas in Practice

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 …

Compositional Reasoning Gotchas in PracticeRead More »

Liveness vs Safety – A Practical Viewpoint

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 …

Liveness vs Safety – A Practical ViewpointRead More »

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.

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

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.