Improving Constrained Random Pattern Generation by Powerful Global and Local Infeasible Solution Space Identification
Date Issued
2015
Date
2015
Author(s)
Lin, En-Hsiang
Abstract
Functional verification is indispensable in circuit design flow. Directed testing is the most prevalently used method in industry. It can quickly validate basic functionality of design under verification (DUV) at the early stage. However, the generated test vectors are easily biased due to the designers’ perception on the DUV, which lowers the chance to trigger corner bugs. This greatly affects the test coverage of DUV. Another approach called Constraint Random Verification (CRV) draws more attention in recent years. Users provide input constraints based on system specification and their intention for verification, and then a constraint solver would efficiently generate vast amounts of patterns that satisfy the constraints. Compared to former approach, it can quickly generate more effective patterns to simulate the DUV. Constraint solving technique is the key of CRV methodology. A good constraint solver for CRV should have the following properties: 1) high throughput 2) uniform distribution (in probability) 3) high pattern diversity (in search space). In other words, it should efficiently generate valid patterns while ensuring evenness and pattern diversity at the same time. In this thesis, we focus on improving throughput for some rather difficult cases. Our improvements mainly come from the identification of infeasible solution space for the input constraints. Intuitively, as more infeasible solution space is identified, the higher throughput the constraint solver can be achieved. We divide the identification into two stages: 1) global infeasible space identification 2) local infeasible space identification. They apply to different situations. At global infeasible space identification stage, it filters out infeasible space which consists of universally reducible variables. A variable is universally reducible if its initial range can be reduced without consideration of the assignments of other variables. We proposed an iterative event-driven approach combined with the word-level SMT solver to identify such space. At local infeasible space identification stage, remaining infeasible space is mostly composed of conditionally reducible variables. A variable is conditionally reducible if its range can only be reduced with regard to the assignments of some of other variables. We utilize the Range Splitting Tree (RST) technique to filter out such infeasible space. The structure of constructed RST greatly affects the ability of infeasible space identification. Our RST construction is guided by dynamically selecting the constraint with lowest hit rate on-the-fly. Experimental results show the effectiveness of this greedy based construction to identify infeasible space, and thus the throughput can be substantially enhanced.
Subjects
Functional Verification
Constrained Random Verification
Range Splitting Tree
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-104-R97921042-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):980a12852589f8350130301ffff41a23