Functional test generation based on word-level SAT
Saved in:
| Title: | Functional test generation based on word-level SAT |
|---|---|
| Authors: | Zeng, Zhihong1 zzeng@avery-design.com, Talupuru, Kesava R.1 kesava@logic-mill.com, Ciesielski, Maciej ciesiel@ecs.umass.edu |
| Source: | Journal of Systems Architecture. Aug2005, Vol. 51 Issue 8, p488-511. 24p. |
| Subjects: | Slosson Intelligence Test, Mathematics, RTL (Computer program language), Logic programming |
| Abstract: | Abstract: Functional test generation coupled with symbolic simulation offers a good compromise between formal verification and numerical simulation for design validation. The generation of functional test vectors guided by miscellaneous coverage metrics can be posed as a satisfiability problem (SAT). While a number of efficient Boolean SAT engines have been developed for gate level designs, they are not directly applicable to behavioral and RTL designs containing significant arithmetic components. This paper presents two approaches that enhance the capability of functional test generation by preserving arithmetic operators in the design. They are based on word-level SAT techniques: (1) LPSAT, based on integer linear programming, and (2) CLP-SAT, based on constraint logic programming. The proposed SAT solvers allow to efficiently handle the designs with mixed word-level arithmetic operators and bit-level logic gates. The experimental results are quite encouraging compared to traditional CNF-based and BDD-based SAT solvers. The paper also suggests a method to build an integrated SAT solving framework where different SAT solvers work together to provide a more complete solution to functional test generation and other verification applications. [Copyright &y& Elsevier] |
| Copyright of Journal of Systems Architecture is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
Be the first to leave a comment!
