FORMAL: A Sequential ATPG-Based Bounded Model Checking System for VLSI Circuits

 
 
 
 

FORMAL: A Sequential ATPG-Based Bounded Model Checking System for VLSI Circuits

Show full item record


Title: FORMAL: A Sequential ATPG-Based Bounded Model Checking System for VLSI Circuits
Author: Qiang, Qiang
Description: 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.
Permanent Link: http://rave.ohiolink.edu/etdc/view?acc_num=case1144449349
http://hdl.handle.net/2374.OX/16530
Date: 2006

Files in this item

Files Size Format View

There are no files associated with this item.

This item appears in the following Collection(s)

Show full item record