Formal Verification of Combinational Circuits
Abstract
With the increase in the complexity of
present day systems, proving the
correctness of a design has become a major concern.
Simulation based methodologies are generally
inadequate to validate the correctness of a design
with a reasonable confidence. More and more
designers are moving towards formal methods to
guarantee the correctness of their designs.
In this paper we survey some state-of-the-art
techniques used to perform automatic verification of
combinational circuits.
We classify the current approaches for combinational
verification into two categories: functional and
structural. The functional methods consist of
representing a circuit as a canonical decision diagram.
Two circuits are equivalent if and only if their decision
diagrams are equal. The structural methods consist of
identifying related nodes in the circuit and using
them to simplify the problem of verification.
We briefly describe some of the methods in both the categories
and discuss their merits and drawbacks.
For comments contact
anarayan@ic.eecs.berkeley.edu