Tautology checking using cross-controllability and cross-observability relations
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
A novel method is described for verifying the equivalence between a combinational circuit and its specification, when both are given in a modular (e.g., factored) form. It is based on the notion of cross-controllability and cross-observability relations that exist between the internal logic values across a cut of the joint composition of the circuit and the specification. It is proven that even after abstracting input and other internal variables the relations are sufficient to verify the equivalence. The abstraction allows reduction of the size of the relation, thus permitting the verification of much larger circuits. A report is presented on the verification of an 8*8 parallel multiplier using at most 527 BDD (binary decision diagram) cells of 21 variables. Extensions to sequential circuits are also discussed.Keywords
This publication has 5 references indexed in Scilit:
- An algebraic model for asynchronous circuits verificationIEEE Transactions on Computers, 1988
- Verification algorithms for VLSI synthesisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Binary Decision DiagramsIEEE Transactions on Computers, 1978
- An Approach to Unified Methodology of Combinational Switching CircuitsIEEE Transactions on Computers, 1977