Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


case1144614543.pdf (675.28 KB)

ETD Abstract Container

Abstract Header

FORMAL: A SEQUENTIAL ATPG-BASED BOUNDED MODEL CHECKING SYSTEM FOR VLSI CIRCUITS

Qiang, Qiang
http://rave.ohiolink.edu/etdc/view?acc_num=case1144614543

Abstract Details

2006, Doctor of Philosophy, Case Western Reserve University, Computer Engineering.
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 solved by a SAT solver. Automatic Test Pattern Generation (ATPG), as an alternative to SAT, has already been shown an effective solution to NP-complete problems in many computer-aided design areas. In the field of BMC, ATPG has already achieved promising results for simple properties; its effectiveness for more complicated nested properties, however, remains unknown. This thesis presents the first systematic framework of ATPG-based BMC capable of checking properties in all nested forms on gate level. The negation counterpart to a property is mapped into a structural monitor, which is tailored to a flattened model of the input circuit. A target fault is then injected at the monitor output, and a modified ATPG-based state justification algorithm is used to search a test for this fault. Finding such a test corresponds to formally establishing the property. The framework can easily incorporate any existing ATPG tool with little modification. The proposed framework has been implemented in a computer program called FORMAL, and has been used to check a comprehensive set of properties of GL85 microprocessor and USB 2.0 circuits. Experimental results show that the ATPG-based approach performs better in both capacity and efficiency than the SAT-based techniques, especially for large bounds and for properties that require large search space. Therefore, ATPG-based BMC has been demonstrated an effective supplement to SAT-based BMC in VLSI circuit verification.
Daniel Saab (Advisor)
89 p.
Bounded Model Checking; BMC; Automatic Test Pattern Generation; ATPG; Sequential ATPG; Formal Verification; Functional Verification; VLSI Design and Verification

Recommended Citations

Citations

  • Qiang, Q. (2006). FORMAL: A SEQUENTIAL ATPG-BASED BOUNDED MODEL CHECKING SYSTEM FOR VLSI CIRCUITS [Doctoral dissertation, Case Western Reserve University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=case1144614543

    APA Style (7th edition)

  • Qiang, Qiang. FORMAL: A SEQUENTIAL ATPG-BASED BOUNDED MODEL CHECKING SYSTEM FOR VLSI CIRCUITS. 2006. Case Western Reserve University, Doctoral dissertation. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=case1144614543.

    MLA Style (8th edition)

  • Qiang, Qiang. "FORMAL: A SEQUENTIAL ATPG-BASED BOUNDED MODEL CHECKING SYSTEM FOR VLSI CIRCUITS." Doctoral dissertation, Case Western Reserve University, 2006. http://rave.ohiolink.edu/etdc/view?acc_num=case1144614543

    Chicago Manual of Style (17th edition)

case1144614543
1,222
© 2006, all rights reserved.
This open access ETD is published by Case Western Reserve University School of Graduate Studies and OhioLINK.