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

ABSTRACT

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

REFERENCES

• 1: W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954.
• 2: Luís Baptista , João P. Marques Silva, Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming, p.489-494, September 18-21, 2000
• 3: R.J. Bayardo, Jr., and R. Schrag, "Using CSP look-back techniques to solve real world SAT instances," 14th National Conference on Artificial Intelligence (AAAI '97), July 1997, pp. 203-208.
• 4: BED Package 3 , version 2.5, October 2000.
• 5: F. Brglez, and H. Fujiwara, "A Neutral Netlist of 10 Combinational Benchmark Circuits," International Symposium on Circuits and Systems (ISCAS '85), 1985.
• 6: F. Brglez, D. Bryan, and K. Kozminski, "Combinational Profiles of Sequential Benchmark Circuits," International Symposium on Circuits and Systems (ISCAS '89), 1989.
• 7: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 8: Randal E. Bryant , Steven German , Miroslav N. Velev, Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.93-134, Jan. 2001 [doi>10.1145/371282.371364]
• 9: Randal E. Bryant , Miroslav N. Velev, Boolean Satisfiability with Transitivity Constraints, Proceedings of the 12th International Conference on Computer Aided Verification, p.85-98, July 15-19, 2000
• 10: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 11: Multi-resolution on compressed sets of clauses, Proceedings of the 12th IEEE International Conference on Tools with Artificial Intelligence, p.2, November 13-15, 2000
• 12: CGRASP, http://vinci.inesc.pt/~lgs/cgrasp.
• 13: James M. Crawford , Larry D. Auton, Experimental results on the crossover point in random 3-SAT, Artificial Intelligence, v.81 n.1-2, p.31-57, March 1996 [doi>10.1016/0004-3702(95)00046-1]
• 14: CUDD-2.3.0, http://vlsi.colorado.edu/~fabio.
• 15: O. Dubois, "Can a Very Simple Algorithm be Efficient for SAT?", ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/contributed/dubois/.
• 16: Jon William Freeman, Improvements to propositional satisfiability search algorithms, University of Pennsylvania, Philadelphia, PA, 1995
• 17: GRASP, http://vinci.inesc.pt/~jpms/grasp.
• 18: Anuj Goel , Khurram Sajid , Hai Zhou , Adnan Aziz , Vigyan Singhal, BDD Based Procedures for a Theory of Equality with Uninterpreted Functions, Proceedings of the 10th International Conference on Computer Aided Verification, p.244-255, June 28-July 02, 1998
• 19: Carla P. Gomes , Bart Selman , Nuno Crato , Henry Kautz, Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems, Journal of Automated Reasoning, v.24 n.1-2, p.67-100, February 2000 [doi>10.1023/A:1006314320276]
• 20: Jan Friso Groote , Joost P. Warners, The Propositional Formula Checker HeerHugo, Journal of Automated Reasoning, v.24 n.1-2, p.101-125, February 2000 [doi>10.1023/A:1006366304347]
• 21: Ilker Hamzaoglu , Janak H. Patel, New Techniques for Deterministic Test Pattern Generation, Journal of Electronic Testing: Theory and Applications, v.15 n.1-2, p.63-73, August-October 1999 [doi>10.1023/A:1008355411566]
• 22: Justin E. Harlow, III , Franc Brglez, Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.64-81, November 04-06, 1998
• 23: John L. Hennessy , David A. Patterson, Computer architecture (2nd ed.): a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 24: Holger H. Hoos, SAT-Encodings, Search Space Structure, and Local Search Performance, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.296-303, July 31-August 06, 1999
• 25: IA-64 Application Developer's Architecture Guide,5 Intel Corporation, May 1999.
• 26: Kazuo Iwama , Hidetoshi Abeta , Eiji Miyano, Random Generation of Satisfiable and Unsatisfiable CNF Predicates, Proceedings of the IFIP 12th World Computer Congress on Algorithms, Software, Architecture - Information Processing '92, Volume 1, p.322-328, September 07-11, 1992
• 27: Kazuo Iwama , Kensuke Hino, Random generation of test instances for logic optimizers, Proceedings of the 31st annual conference on Design automation, p.430-434, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196452]
• 28: D.S. Johnson, M.A. Trick, eds., The Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science. http://dimacs.rutgers.edu/challenges.
• 29: Priyank Kalla , Zhihong Zeng , Maciej J. Ciesielski , Chilai Huang, A BDD-based satisfiability infrastructure using the unate recursive paradigm, Proceedings of the conference on Design, automation and test in Europe, p.232-236, March 27-30, 2000, Paris, France [doi>10.1145/343647.343769]
• 30: C.M. Li, and Anbulagan, "Heurisitics Based on Unit Propoagation for Satisfiability Problems," International Joint Conference on Artificial Intelligence (IJCAI '97), August 1997, pp. 366-371.
• 31: Chu Min Li, Integrating Equivalency Reasoning into Davis-Putnam Procedure, Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, p.291-296, July 30-August 03, 2000
• 32: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 33: João P. Marques Silva, The Impact of Branching Heuristics in Propositional Satisfiability Algorithms, Proceedings of the 9th Portuguese Conference on Artificial Intelligence: Progress in Artificial Intelligence, p.62-74, September 21-24, 1999
• 34: J.P. Marques-Silva, and L.G. e Silva, 'Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning,"2 12th Symposium on Integrated Circuits and Systems Design (SBCCI '99), September - October 1999, pp. 192-195.
• 35: João P. Marques Silva, Algebraic Simplification Techniques for Propositional Satisfiability, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming, p.537-542, September 18-21, 2000
• 36: D. Mitchell, B. Selman, and H. Levesque, "Hard and Easy Distributions of SAT Problems," 10th National Conference on Artificial Intelligence (AAAI '92), July 1992, pp. 459-465.
• 37: S. Malik, A.R. Wang, R.K. Brayton, and A. Sangiovani-Vincentelli, "Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment," International Conference on Computer-AIded Design (ICCAD '88), November 1988, pp. 6-9.
• 38: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 39: D.A. Plaisted, A. Biere, and Y. Zhu, "A Satisfiability Procedure for Quantified Boolean Formulae," submitted for publication, 2000.
• 40: Amir Pnueli , Yoav Rodeh , Ofer Shtrichman , Michael Siegel, Deciding Equality Formulas by Small Domains Instantiations, Proceedings of the 11th International Conference on Computer Aided Verification, p.455-469, July 06-10, 1999
• 41: S.D. Prestwich, "Stochastic Local Search in Constrained Spaces," Practical Application of Constraint Technology and Logic Programming (PACLP '00), April 2000, pp. 27-39.
• 42: Jussi Rintanen, Improvements to the Evaluation of Quantified Boolean Formulae, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.1192-1197, July 31-August 06, 1999
• 43: Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
• 44: SATO.3.2.1, http://www.cs.uiowa.edu/~hzhang/sato.
• 45: SATLIB-Solvers, http://www.satlib.org/solvers.html.
• 46: B. Selman, H. Kautz, B. Cohen, "Local Search Strategies for Satisfiability Testing," DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 26 (1996), pp. 521-532.
• 47: B. Selman, and H. Kautz, "Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems," International Joint Conference on Artificial Intelligence (IJCAI '93), August - September 1993, pp. 290-295.
• 48: Yi Shang , Benjamin W. Wah, A Discrete Lagrangian-Based Global-SearchMethod for Solving Satisfiability Problems, Journal of Global Optimization, v.12 n.1, p.61-99, January 1998 [doi>10.1023/A:1008287028851]
• 49: H. Sharangpani, "Intel Itanium Processor Michroarchitecture Overview,"5 Microprocessor Forum, October 1999.
• 50: G. StAlmarck, "A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula," Swedish Patent No. 467 076 (approved 1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995), 1989.
• 51: Stanford Validity Checker (SVC), http://sprout.Stanford.EDU/SVC.
• 52: P. Tafertshofer, A. Ganz, and K.J. Antreich, "GRAINE-An Implication GRaph-bAsed engINE for Fast Implication, Justification, and Propagation," IEEE Transactions on CAD, Vol. 19, No. 8 (August 2000).
• 53: David Tennenhouse, Proactive computing, Communications of the ACM, v.43 n.5, p.43-50, May 2000 [doi>10.1145/332833.332837]
• 54: David Van Campenhout , Trevor Mudge , John P. Hayes, Collection and Analysis of Microprocessor Design Errors, IEEE Design & Test, v.17 n.4, p.51-60, October 2000 [doi>10.1109/54.895006]
• 55: Miroslav N. Velev , Randal E. Bryant, Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.37-53, September 27-29, 1999
• 56: Miroslav N. Velev , Randal E. Bryant, Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction, Proceedings of the 37th conference on Design automation, p.112-117, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337331]
• 57: Miroslav N. Velev, Formal Verification of VLIW Microprocessors with Speculative Execution, Proceedings of the 12th International Conference on Computer Aided Verification, p.296-311, July 15-19, 2000
• 58: M.N. Velev, Benchmark suites 4 SSS-SAT.1.0, VLIW-SAT.1.0, FVP-UNSAT.1.0, and FVP-UNSAT.2.0, October 2000.
• 59: Miroslav N. Velev, Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.252-267, April 02-06, 2001
• 60: Poul Frederick Williams , Armin Biere , Edmund M. Clarke , Anubhav Gupta, Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, p.124-138, July 15-19, 2000
• 61: P.F. Williams, "Formal Verification Based on Boolean Expression Diagrams,"3 Ph.D. thesis, Department of Information Technology, Technical University of Denmark, Lyngby, Denmark, August 2000.
• 62: Zhe Wu , Benjamin W. Wah, Solving Hard Satisfiability Problems: A Unified Algorithm Based on Discrete Lagrange Multipliers, Proceedings of the 11th IEEE International Conference on Tools with Artificial Intelligence, p.210, November 08-10, 1999
• 63: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

Additional Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Instruction set design (e.g., RISC, CISC, VLIW)

  J. Computer Applications
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.2 Installation Management
          Subjects: Benchmarks

General Terms:
Design, Measurement, Performance, Reliability, Standardization, Theory, Verification