Name
Abstract | ||
|---|---|---|
A major technique to address state explosion problem in model checking is abstraction. Predicate abstraction has been applied successfully to large software and now to hardware descriptions, such as Verilog. This paper evaluates the state-of-the-art constraint logic programming (CLP) techniques to improve the performance of predication abstraction of hardware designs, and compared it with the SAT-based predicate abstraction techniques. With CLP based techniques, we can model various constraints, such as bit, bit-vector and integer, in a uniform framework; we can also model the word-level constraints without flatting them into bit-level constraints as SAT-based method does. With these advantages, the computation of abstraction system can be more efficient than SAT-based techniques. We have implemented this method, and the experimental results have shown the promising improvements on the performance of predicate abstraction of hardware designs. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11562948_15 | ATVA |
Keywords | Field | DocType |
sat-based method,bit-level constraint,model checking,hardware description,abstraction system,predicate abstraction,constraint logic programming,hardware design,sat-based technique,rtl verilog description,predication abstraction,sat-based predicate abstraction technique | Abstraction model checking,Constraint satisfaction,Model checking,Abstraction,Predicate abstraction,Computer science,Theoretical computer science,Abstraction inversion,Verilog,Constraint logic programming | Conference |
Volume | ISSN | ISBN |
3707 | 0302-9743 | 3-540-29209-8 |
Citations | PageRank | References |
1 | 0.36 | 12 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tun Li | 1 | 43 | 14.97 |
| Yang Guo | 2 | 16 | 4.18 |
| Sikun Li | 3 | 224 | 44.71 |
| GongJie Liu | 4 | 6 | 1.51 |