الفهرس 
INTRODUCTION TO FORMAL HARDWARE VERIFICATIONOnly 14 pages are availabe for public view
 |  | from | 136 |  |  |
| | | from | 136 | | |
Abstract
Formal verification of digital circuits became an active research area in the
last two decades. The pioneering work of Randal E. Bryant on Binary
Decision Diagrams started a lot of research in this area. In addition, the shift
of the design methodology from the schematic based to hardware description
languages facilitates the introduction of formal verification in the design
flow.
In this thesis, we focus on the combinational equivalence checking problem.
We propose and implement three novel approaches. The first approach is
based on reducing the search tree of the Boolean satisfiability formula using
binary decision diagrams. The second approach integrates recursive learning
and global implications in an iterative method. The third approach
decomposes the circuits under verification and makes use of Boolean
satisfiability, binary decision diagrams and functional learning to prove the
circuit. In addition, we present a general verification framework where the
different verification engines act as filters.
We also extend our work to sequential circuits. We study the reachability
analysis problems of finite state machines. We show how don’t cares can be
used to reduce the transition relation BOD during symbolic image
computation. We also perform reachability analysis using Boolean
satisfiability and logic minimization techniques. Finally, sequential circuit
verification based on the proposed techniques is studied and implemented.
For this thesis, the tool M-CHECK has been implemented in C for UN1X
operating systems. The tool acts as a framework where the different ideas
and algorithms are implemented and tested. The tool features 23 commands
and it has been efficiently used to verify the ISCAS’85 benchmarks and
industrial circuits of size up to lOOK gates.
Keywords: Equivalence Checking, SAT, BODs, Recursive Learning,
Global Implications, Verification flow, ATPG, FSM symbolic traversal.