Name
Abstract | ||
|---|---|---|
We present a novel approach to static check properties for RT-Level design verification. Our approach combines program-slicing based static design extraction, word-level SAT solving and dynamic searching techniques. The design extraction makes property-checking concentrate on the design parts related to the given properties, thus large practical designs can be handled. Constraint Logic Programming (CLP) naturally models mixed bit-level and word-level constraints, and word-level SAT technique effectively solves the mixed constraints in a unified framework, which greatly improves the performance of property checking. Initial searching states derived from dynamic simulation dramatically accelerate the searching process of property checking. A prototype system has been built, and the experimental results on some public benchmark and industrial circuits demonstrate the efficiency of our approach and its applicability to large practical designs. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-30476-0_44 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
program slicing,dynamic simulation | Constraint satisfaction,Model checking,Computer science,Slicing,Propositional calculus,Algorithm,Program analysis,Constraint logic programming,Electronic circuit,Computer engineering,Dynamic simulation,Distributed computing | Conference |
Volume | ISSN | Citations |
3299 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 7 | 3 |