Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


case1159738055.pdf (376.01 KB)

ETD Abstract Container

Abstract Header

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

Ou, Jen-Chieh
http://rave.ohiolink.edu/etdc/view?acc_num=case1159738055

Abstract Details

2007, Doctor of Philosophy, Case Western Reserve University, Computer Engineering.
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.
Daniel Saab (Advisor)
Slicing; veri¿¿¿¿¿¿cation; Program Slicing; Verilog; RTL

Recommended Citations

Citations

  • Ou, J.-C. (2007). HARDWARE DESCRIPTION LANGUAGE PROGRAM SLICING AND WAY TO REDUCE BOUNDED MODEL CHECKING SEARCH OVERHEAD [Doctoral dissertation, Case Western Reserve University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=case1159738055

    APA Style (7th edition)

  • Ou, Jen-Chieh. HARDWARE DESCRIPTION LANGUAGE PROGRAM SLICING AND WAY TO REDUCE BOUNDED MODEL CHECKING SEARCH OVERHEAD. 2007. Case Western Reserve University, Doctoral dissertation. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=case1159738055.

    MLA Style (8th edition)

  • Ou, Jen-Chieh. "HARDWARE DESCRIPTION LANGUAGE PROGRAM SLICING AND WAY TO REDUCE BOUNDED MODEL CHECKING SEARCH OVERHEAD." Doctoral dissertation, Case Western Reserve University, 2007. http://rave.ohiolink.edu/etdc/view?acc_num=case1159738055

    Chicago Manual of Style (17th edition)

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