HARDWARE DESCRIPTION LANGUAGE PROGRAM SLICING AND WAY TO REDUCE BOUNDED MODEL CHECKING SEARCH OVERHEAD

Now showing item 1 of 1

Title:	HARDWARE DESCRIPTION LANGUAGE PROGRAM SLICING AND WAY TO REDUCE BOUNDED MODEL CHECKING SEARCH OVERHEAD
Author:	Ou, Jen-Chieh
Description:	Modern complex digital systems are described in Hardware Description Language (HDL). The increase in design complexity is causing verification tools to require large amount of resources. In this research, we present a program slicing technique to extract statements from an RTL design that directly or indirectly contribute to a formal verification rule. The extracted statements constitute a less complex design that reduces the resource needed by verification tools without compromising the quality of the result. Both static and conditioned Verilog slicer is implemented in a computer program that is used as a pre-processor to SAT-based bounded model checker SMV and ATPG-based bounded model checker Formal. We show experimentally that the resources of the formal verification tool in terms of both CPU and memory are reduced significantly when verifying the USB2.0 IP core. The proposed slicer is the first hardware slicing technique that handles inter-module signal dependency in a hierarchical Verilog design environment.
Permanent Link:	http://rave.ohiolink.edu/etdc/view?acc_num=case1159738055 http://hdl.handle.net/2374.OX/16917
Date:	2007

Files in this item

Files	Size	Format	View
There are no files associated with this item.

Now showing item 1 of 1