An efficient finite-domain constraint solver for circuits

ABSTRACT

We present a novel hybrid finite-domain constraint solving engine for RTL circuits, that automatically uses data-path abstraction. We describe how DPLL search can be modified by using efficient finite-domain constraint propagation to improve communication between interacting integer and Boolean domains. This enables efficient combination of Boolean SAT and linear integer arithmetic solving techniques. We use conflict-based learning using the variables on the boundary of control and data-path for additional performance benefits. Finally, the hybrid constraint solver is experimentally analyzed using some example circuits.

REFERENCES

• 1: Abramovici, M., Breuer, M. A., and Friedman, A. D. Digital Systems Testing and Testable Design, 1$^st$ ed. Computer Science Press, 1990.
• 2: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 3: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation, p.522-527, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277186]
• 4: Raik Brinkmann , Rolf Drechsler, RTL-Datapath Verification using Integer Linear Programming, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.741, January 07-11, 2002
• 5: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 6: Dantzig, G., and Eaves, B. Fourier-motzkin elimination and its dual. Journal of Combinatorial Theory A, 14 (1973), 288--297.
• 7: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 8: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 9: R. Drechsler, B. Becker, and S. Ruppertz. K*BMDs: a new data structure for verification. In IFI WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods Frankfurt, Germany, October 1995.
• 10: Warwick Harvey , Peter J. Stuckey, Improving Linear Constraint Propagation by Changing Constraint Representation, Constraints, v.8 n.2, p.173-207, April 2003 [doi>10.1023/A:1022323717928]
• 11: Chung-Yang Huang , Kwang-Ting Cheng, Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques, Proceedings of the 37th conference on Design automation, p.118-123, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337333]
• 12: Iyer, M. A. RACE: A Word-Level ATPG-Based Constraints Solver System For Smart Random Simulation In Proc. of the ITC (2003), pp. 259--266.
• 13: M. K. Iyer , G. Parthasarathy , K.-T. Cheng, SATORI - A Fast Sequential SAT Engine for Circuits, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.320, November 09-13, 2003 [doi>10.1109/ICCAD.2003.122]
• 14: W. Kelly, V. Maslow, W. Pugh, et. al. The Omega Calculator and Library v1.1.0. Tech. rep., Dept. of CS, University of Maryland, College Park, November 1996.
• 15: Cong Liu , Andreas Kuehlmann , Matthew W. Moskewicz, CAMA: A Multi-Valued Satisfiability Solver, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.326, November 09-13, 2003 [doi>10.1109/ICCAD.2003.45]
• 16: 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]
• 17: 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]
• 18: R.M. Stallman, and G.J. Sussman. Forward Reasoning and Dependency Directed Backtracking in a System for Computer Aided Circuit Analysis". Artificial Intelligence 9, 2 (1977), 135--196.
• 19: Ofer Strichman, On Solving Presburger and Linear Arithmetic with SAT, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.160-170, November 06-08, 2002
• 20: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.0 General

General Terms:
Algorithms

Keywords:
bit-vector arithmetic, boolean satisfiability, circuits, constraints, decision procedures, design verification, integer linear programming