Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors
作者： M.N. Velev , R.E. Bryant
关键词:
摘要: We compare SAT-checkers and decision diagrams on the evaluation of Boolean formulas produced in formal verification both correct buggy versions superscalar VLIW microprocessors. identify one SAT-checker that significantly outperforms rest. evaluate ways to enhance its performance by variations generation correctness formulas. reassess optimizations previously used speed up probe future challenges.
sci-hub.se 参考文章(43)
Bart Selman, David Mitchell, Hector Levesque, Hard and easy distributions of SAT problems national conference on artificial intelligence. pp. 459- 465 ,(1992)
João P. Marques-Silva, Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning ,(1999)
Holger H. Hoos, SAT-encodings, search space structure, and local search performance international joint conference on artificial intelligence. pp. 296- 302 ,(1999)
Bart Selman, Henry Kautz, Domain-independent extensions to GSAT: solving large structured satisfiability problems international joint conference on artificial intelligence. pp. 290- 295 ,(1993)
Jussi Rintanen, Improvements to the evaluation of quantified boolean formulae international joint conference on artificial intelligence. pp. 1192- 1197 ,(1999)
Justin E. Harlow, Franc Brglez, Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations formal methods in computer aided design. pp. 64- 81 ,(1998) , 10.1007/3-540-49519-3_6
Miroslav N. Velev, Randal E. Bryant, Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic Lecture Notes in Computer Science. pp. 37- 53 ,(1999) , 10.1007/3-540-48153-2_5
Hantao Zhang, SATO: An Efficient Propositional Prover conference on automated deduction. pp. 272- 275 ,(1997) , 10.1007/3-540-63104-6_28
Miroslav N. Velev, Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors tools and algorithms for construction and analysis of systems. pp. 252- 267 ,(2001) , 10.1007/3-540-45319-9_18
Yi Shang, Benjamin W. Wah, A Discrete Lagrangian-Based Global-SearchMethod for Solving Satisfiability Problems Journal of Global Optimization. ,vol. 12, pp. 61- 99 ,(1998) , 10.1023/A:1008287028851