Coverage-Based Microprocessor Verification

Formal Microprocessor Verification

Microprocessors are subject to subtle design errors. Unfortunately, the complexity of processors is outstripping the capacity of conventional methods, primarily simulation, to debug them before fabrication. Simulation of commercial microprocessors is consuming vast resources in terms of machines, workers, and, most importantly, time-to-market.

It is hoped that formal verification techniques can help solve this problem. But, for this hope to be realistic, the labor required to do formal verification must be reduced by orders-of-magnitude.

ormal verification must be reduced by orders-of-magnitude.
• Formal Verification Technology for Microprocessors - Stanford
• Computer-assisted Formal Verification of Microprocessor Pipeline Control - Dr. Dill - Stanford
• Formal Verification of a Microprocessor with Security Features - U of Idaho

  This project focuses on the formal specification and verification of a pipelined RISC microprocessor with security features. The design includes all aspects of microprocessor design from the high-level formal specification of the macro programming level to the fabrication and testing of the actual microprocessor.

• Binary Decision Diagrams and Beyond: Enabling Technologies For Formal Verification - ICCAD 95 - Randal E. Bryant - Carnegie Mellon Univ.
  Ordered Binary Decision Diagrams (OBDDs) have found widespread use in CAD applications such as formal verification, logic synthesis, and test generation. OBDDs represent Boolean functions in a form that is both canonical and compact for many practical cases. They can also be generated and manipulated by efficient graph algorithms. Researchers have found that many CAD tasks can be expressed as series of operations on Boolean functions, making them candidates for OBDD-based methods.
  The success of OBDDs has inspired efforts to improve their efficiency and to expand their range of applicability. Techniques have been discovered to make the representation more compact and to represent other classes of functions. This has led to improved performance on existing OBDD applications, as well as enabled new classes of problems to be solved.
  An unfortunate byproduct of the dynamic and widespread research community in this area has been a proliferation of names and terminology, leading to an "alphabet soup" of acronyms. The following is only a partial list: OBDD, FBDD, FDD, OKFDD, EVBDD, MTBDD, BMD, *BMD, ZBDD, ABDD, HDD, TDD, and OPDD. Keeping track of the developments and how they relate to one another is a challenging task.
  This tutorial will provide an overview of the state of the art in graph-based function representations and their applications to CAD. It will provide a unified framework for the different representations as well as describe their practical impact. Several applications of BDDs will be studied both successes and failures in an attempt to characterize their suitability for CAD applications.
• VERILAT: Verification Using Logic Augmentations And Transformations

  This paper presents a new framework for formal logic verification. What is depicted here is fundamentally different from previous approaches. In earlier approaches, the circuit is either not changed during the verification process, as in OBDD or implication-based methods, or the circuit is progressively reduced during verification. Whereas this approach actually enlarge the circuits by adding gates during the verification process. Specifically introduced here is a new technique that transforms the reference circuit as well as the circuit to be verified, so that the similarity between the two is progressively enhanced. This requires addition of gates to the reference circuit and/or the circuit to be verified. In the process, they reduce the dissimilarity between the two circuits, which makes it easier to verify the circuits.

Related Links

• Abstract Hardware Limited
  Has developed LAMBDA a system synthesis tool that automatically applies formal verification during the design process rather than post design process as is the case with most formal ver methodologies/tools.




---

[Coverage-Based Ver] [Formal Ver] [Formal Hardware Ver] [Knowledge-Based Ver]

---