Improving Simulation-Based and Formal Verification Techniques by Automatic High-Level Design Intent and Invariant Extractions
Date Issued
2012
Date
2012
Author(s)
Yeh, Hu-Hsi
Abstract
In the dissertation, we build an open source RTL framework, QuteRTL, which can serves as a front-end for the researches in RTL synthesis and verification. Users can use our framework to read in RTL Verilog designs, obtain CDFGs, extract high-level design information (e.g. FSM), generate hierarchical or flattened gate-level netlists, and link with logic synthesis tools (e.g. Berkeley ABC). Various research opportunities will be made possible by this framework, such as RTL debugging, word-level formal engines, design abstraction, and a complete open-source RTL-to-gate tool chain, etc. In addition, we also devise systematic and robust algorithms that can automatically extract high level design intents from complex RTL Designs, and then utilize them to assist both simulation and formal verification.
For simulation, we proposed an Automatic Target Constraint Generation (ATCG) technique to automatically generate compact and high-quality constraints for the guided random simulation environment. Our objective is to tackle the biggest bottleneck of the entire constrained random simulation process ─ the time-consuming and error-prone manual testbench composition process. The proposed approach alleviates the users’ burden in manually writing constraints for the constrained random simulation environment. Our experimental results show that ATCG can outperform both directed and random simulations in both coverage and simulation runtime for a variety of designs.
For formal verification, we propose a property-specific sequential invariant extraction algorithm to improve the performance of the SAT-based unbounded modeling checkers (UMCs). By analyzing the property-related predicates and their corresponding high-level design constructs such as FSMs and counters, we can quickly identify the sequential invariants that are useful in improving the property proving capabilities. We utilize these sequential invariants to refine the inductive hypothesis in induction-based UMCs, and to improve the accuracy of reachable state approximation in interpolation-based UMCs. The experimental results show that our tool can outperform a state-of-the-art UMC in most cases, especially for the difficult true properties.
Subjects
Constraint generation
constraint guided simulation
function verification
testbench authoring
model checking
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-101-F93943122-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):17a8c6102da8b527eb6bb4097e4c94ff