FORMAL: A SEQUENTIAL ATPG-BASED BOUNDED MODEL CHECKING SYSTEM FOR VLSI CIRCUITS
Qiang Qiang · OhioLink ETD Center (Ohio Library and Information Network) · 2006
Bounded Model Checking (BMC) is a formal method of verifying Very Large Scale Integrated (VLSI) circuits.It shows violation of a given circuit property by finding a counter-example to the property along bounded state paths of the circuit.The BMC problem is inherently NP-complete and is traditionally formulated to a boolean SATisfiability (SAT) problem, which is subsequently First of all, I would like to acknowledge the leading role in my academic and professional path -my adviser, Prof. Daniel G. Saab.Special thanks are given to his vision in motivating me into a lifelong career in Computer Engineering, to his advisory skills in guiding me throughout my Ph.D.