Title page for ETD etd-06152007-151253


Type of Document Master's Thesis
Author Parikh, Ankur
Author's Email Address aparikh@vt.edu
URN etd-06152007-151253
Title Abstraction Guided Semi-formal Verification
Degree Master of Science
Department Electrical and Computer Engineering
Advisory Committee
Advisor Name Title
Hsiao, Michael S. Committee Chair
Schaumont, Patrick Robert Committee Member
Shukla, Sandeep K. Committee Member
Keywords
  • simulation
  • model checking
  • preimage
  • concretization
  • Hamming distance
  • guided simulation
  • refinement
  • formal verification
  • semi-formal verification
  • abstraction
Date of Defense 2007-06-15
Availability unrestricted
Abstract
Abstraction-guided simulation is a promising semi-formal framework for design validation in which an abstract model of the design is used to guide a logic simulator towards a target property. However, key issues still need to be addressed before this framework can truly deliver on it's promise. Concretizing, or finding a real trace from an abstract trace, remains a hard problem. Abstract traces are often spurious, for which no corresponding real trace exits. This is a direct consequence of the abstraction being an over-approximation of the real design. Further, the way in which the abstract model is constructed is an open-ended problem which has a great impact on the performance of the simulator.

In this work, we propose a novel approaches to address these issues. First, we present a genetic algorithm to select sets of state variables directly from the gate-level net-list of the design, which are highly correlated to the target property. The sets of selected variables are used to build the Partition Navigation Tracks (PNTs). PNTs capture the behavior of expanded portions of the state space as they related to the target property. Moreover, the computation and storage costs of the PNTs is small, making them scale well to large designs.

Our experiments show that we are able to reach many more hard-to-reach states using our proposed techniques, compared to state-of-the-art methods.

Next, we propose a novel abstraction strengthening technique, where the abstract design is constrained to make it more closely resemble the concrete design. Abstraction strengthening greatly reduces the need to refine the abstract model

for hard to reach properties. To achieve this, we efficiently identify sequentially unreachable partial sates in the concrete design via intelligent partitioning, resolution and cube enlargement. Then, these partial states are added as constraints in the abstract model. Our experiments show that the cost to compute these constraints is low and the abstract traces obtained from the strengthened abstract model are far easier to concretize.

Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  thesis_ankur_v3.pdf 504.99 Kb 00:02:20 00:01:12 00:01:03 00:00:31 00:00:02

Browse All Available ETDs by ( Author | Department )

dla home
etds imagebase journals news ereserve special collections
virgnia tech home contact dla university libraries

If you have questions or technical problems, please Contact DLA.