Bounded Model Checking (BMC), as a formal method of verifying VLSI circuits, shows violation of a given circuit property by finding a counter-example to the property along bounded state paths of the circuit. In this paper, we present an emulation framework for Automatic Test Pattern Generation (ATPG)-BMC model capable of checking properties on gate-level design. In our approach, counterpart to a property is mapped into a structural monitor with one output. A target fault is then injected at the monitor output, and a modified ATPG-based state justification algorithm is used to find a test for this fault which corresponds to formally establishing the property. In this paper, emulating the process of ATPG-based BMC on reconfigurable hardware is presented. The ATPG-BMC emulator achieves a speed-up over software based methods, due to the fine-grain massive parallelism inherent to hardware. As circuit sizes approach limits of even ATPG-based method feasibility, further solutions are required. In this presentation, we propose an ATPG-based algorithm for formal verification implementation on reconfigurable hardware (FPGA). This implementation is shown to have a linear relationship between the size of the circuit being verified and FPGA resource utilization. This implies a reasonable bound on the size of the implementation, as opposed to an exponential utilization explosion as circuit size increases.

We have newly introduced the expert designer/user session (EDS) to ISPD in 2013, which is tailor-made for designers and users of physical design (PD) tools. Since ISPD is the premium PD-centric symposium, it is a great opportunity for designers, tools developers and PD researchers to interact and learn from each other. The benefit of including EDS in ISPD's program is twofold.