Robust Boolean reasoning for equivalence checking and functional property verification

Many tasks in computer-aided design (CAD), such as equivalence checking, property checking, logic synthesis, and false paths analysis, require efficient Boolean reasoning for problems derived from circuits. Traditionally, canonical representations, e.g., binary decision diagrams (BDDs), or structura...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computer-aided design of integrated circuits and systems 2002-12, Vol.21 (12), p.1377-1394
Main Authors: Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.
Format: Article
Language:English
Subjects:
Algorithms
Application software
Boolean algebra
Boolean functions
Circuit synthesis
Circuit testing
Computer aided design
Data structures
Design automation
Design engineering
Heuristic
Logic circuits
Logic design
Logic testing
Reasoning
Representations
Robustness
Strength
Studies
Tasks
Transformations
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Many tasks in computer-aided design (CAD), such as equivalence checking, property checking, logic synthesis, and false paths analysis, require efficient Boolean reasoning for problems derived from circuits. Traditionally, canonical representations, e.g., binary decision diagrams (BDDs), or structural satisfiability (SAT) methods, are used to solve different problem instances. Each of these techniques offer specific strengths that make them efficient for particular problem structures. However, neither structural techniques based on SAT, nor functional methods using BDDs offer an overall robust reasoning mechanism that works reliably for a broad set of applications. The authors present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, an SAT procedure, and random simulation natively working on a shared graph representation of the problem. The described intertwined integration of the four techniques results in a powerful summation of their orthogonal strengths. The presented reasoning technique was mainly developed for formal equivalence checking and property verification but can equally be used in other CAD applications. The authors' experiments demonstrate the effectiveness of the approach for a broad set of applications.
ISSN:0278-0070
1937-4151
DOI:10.1109/TCAD.2002.804386