Type of Document Master's Thesis Author Parikh, Ankur Author's Email Address email@example.com 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
- model checking
- Hamming distance
- guided simulation
- formal verification
- semi-formal verification
Date of Defense 2007-06-15 Availability unrestricted AbstractAbstraction-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.
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
If you have questions or technical problems, please Contact DLA.