الفهرس 
Chapter 1Only 14 pages are availabe for public view
 |  | from | 142 |  |  |
| | | from | 142 | | |
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 UNIX 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 I OOK gates.