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
Michael Hsiao	Committee Chair
Patrick Schaumont	Committee Member
Sandeep Shukla	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)
Filename		Size	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