Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors

被引：0

作者：

Velev, MN ^{[1
]}

Bryant, RE ^{[1
]}

机构：

[1] Carnegie Mellon Univ, Dept Elect & Comp Engn, Pittsburgh, PA 15213 USA

来源：

38TH DESIGN AUTOMATION CONFERENCE PROCEEDINGS 2001 | 2001年

关键词：

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We compare SAT-checkers and decision diagrams on the evaluation of Boolean formulas produced in the formal verification of both correct and buggy versions of superscalar and VLIW microprocessors. We identify one SAT-checker that significantly outperforms the rest. We evaluate ways to enhance its performance by variations in the generation of the Boolean correctness formulas We reassess optimizations previously used to speed up the formal verification and probe future challenges.

引用

页码：226 / 231

页数：6

共 6 条

[1] Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors
Velev, MN
Bryant, RE
[J]. JOURNAL OF SYMBOLIC COMPUTATION, 2003, 35 (02) : 73 - 106
[2] Formal verification techniques based on Boolean satisfiability problem
Li, XW
Li, GH
Shao, M
[J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2005, 20 (01): : 38 - 47
[3] Formal Verification Techniques Based on Boolean Satisfiability Problem
Xiao-Wei Li
Guang-Hui Li
Ming Shao
[J]. Journal of Computer Science and Technology, 2005, 20 : 38 - 47
[4] Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction
Velev, MN
Bryant, RE
[J]. 37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 112 - 117
[5] Efficient translation of boolean formulas to CNF in formal verification of microprocessors
Velev, MN
[J]. ASP-DAC 2004: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2004, : 310 - 315
[6] Formal Verification of Modular Multipliers using Symbolic Computer Algebra and Boolean Satisfiability
Mahzoon, Alireza
Grosse, Daniel
Scholl, Christoph
Konrad, Alexander
Drechsler, Rolf
[J]. PROCEEDINGS OF THE 59TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, DAC 2022, 2022, : 1183 - 1188

← 1 →