Advertisement

Improvements to Satisfiability-Based Boolean Function Bi-Decomposition

  • Huan Chen
  • Joao Marques-Silva
Conference paper
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT, volume 379)

Abstract

Boolean function bi-decomposition is pervasive in logic synthesis. Bi-decomposition entails the decomposition of a Boolean function into two other functions connected by a simple two-input gate. Existing solutions are based on Binary Decision Diagrams (BDDs) and, more recently, on Boolean Satisfiability (SAT). Recent work exploited the identification of Minimally Unsatisfiable Subformulas (MUSes) for computing the sets of variables to use in Boolean function bi-decomposition. This paper develops new techniques for improving the use of MUSes in function bi-decomposition. The first technique exploits structural properties of the function being decomposed, whereas the second technique exploits group-oriented MUSes. Experimental results obtained on representative benchmarks from logic synthesis demonstrate significant improvements both in performance and in the quality of decompositions.

Keywords

bi-decomposition logic synthesis satisfiability MUS group-oriented MUS 

References

  1. 1.
    Ashenhurst, R.: The decomposition of switching functions. In: Proceedings of an International Symposium on the Theory of Switching, pp. 74–116 (1957)Google Scholar
  2. 2.
    Curtis, H.: A new approach to the design of switching circuits. Van Nostrand, Princeton (1962)Google Scholar
  3. 3.
    Lai, Y., Pedram, M., Vrudhula, S.: BDD based decomposition of logic functions with application to FPGA synthesis. In: Design Automation Conference, pp. 642–647 (1993)Google Scholar
  4. 4.
    Luba, T., Selvaraj, H.: A general approach to boolean function decomposition and its application in FPGA-based synthesis. VLSI Design 3(3-4), 289–300 (1995)CrossRefGoogle Scholar
  5. 5.
    Scholl, C.: Functional decomposition with application to FPGA synthesis. Springer, Netherlands (2001)zbMATHGoogle Scholar
  6. 6.
    Bochmann, D., Dresig, F., Steinbach, B.: A new decomposition method for multilevel circuit design. In: Proceedings of the European Conference on Design Automation, pp. 374–377 (1991)Google Scholar
  7. 7.
    Sasao, T., Butler, J.T.: On bi-decomposition of logic functions. In: International Workshop on Logic and Synthesis, pp. 1–6 (1997)Google Scholar
  8. 8.
    Mishchenko, A., Steinbach, B., Perkowski, M.: An algorithm for bi-decomposition of logic functions. In: Design Automation Conference, pp. 103–108 (2001)Google Scholar
  9. 9.
    Cortadella, J.: Timing-driven logic bi-decomposition. IEEE Transactions on Computer-Aided Design 22(6), 675–685 (2003)CrossRefGoogle Scholar
  10. 10.
    Steinbach, B., Lang, C.: Exploiting functional properties of boolean functions for optimal multi-level design by bi-decomposition. Artificial Intelligence Review 20(3), 319–360 (2003)zbMATHCrossRefGoogle Scholar
  11. 11.
    Lee, R.R., Jiang, J.H., Hung, W.L.: Bi-decomposing large boolean functions via interpolation and satisfiability solving. In: Design Automation Conference, pp. 636–641 (2008)Google Scholar
  12. 12.
    Choudhury, M., Mohanram, K.: Bi-decomposition of large boolean functions using blocking edge graphs. In: International Conference on Computer-Aided Design, pp. 586–591 (2010)Google Scholar
  13. 13.
    Lin, H.P., Jiang, J.H., Lee, R.R.: To SAT or not to SAT: Ashenhurst decomposition in a large scale. In: International Conference on Computer-Aided Design, pp. 32–37 (2008)Google Scholar
  14. 14.
    Malik, A., Harrison, D., Brayton, R.: Three-level decomposition with application to PLDs. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 628–633 (1991)Google Scholar
  15. 15.
    Sasao, T.: A design method for AND-OR-EXOR three-level networks. In: International Workshop on Logic and Synthesis, pp. 8:11–8:20 (1995)Google Scholar
  16. 16.
    Stanion, T., Sechen, C.: Quasi-algebraic decomposition of switching functions. In: Proceedings of the 16th Conference on Advanced Research in VLSI (ARVLSI), pp. 358–367 (1995)Google Scholar
  17. 17.
    Chang, S., Marek-Sadowska, M., Hwang, T.: Technology mapping for TLU FPGA’s based on decomposition of binary decision diagrams. IEEE Transactions on Computer-Aided Design 15(10), 1226–1236 (1996)CrossRefGoogle Scholar
  18. 18.
    Jiang, J.H., Lee, C.C., Mishchenko, A., Huang, C.Y.: To SAT or not to SAT: Scalable exploration of functional dependency. IEEE Transactions on Computers 59(4), 457–467 (2010)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Liffiton, M., Sakallah, K.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40(1), 1–33 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  20. 20.
    Khasidashvili, Z., Kaiss, D., Bustan, D.: A compositional theory for post-reboot observational equivalence checking of hardware. In: Formal Methods in Computer-Aided Design, pp. 136–143 (2009)Google Scholar
  21. 21.
    Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Formal Methods in Computer-Aided Design (2010)Google Scholar
  22. 22.
    Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Refinement strategies for verification methods based on datapath abstraction. In: Asia and South Pacific Design Automation Conference, pp. 19–24 (2006)Google Scholar
  23. 23.
    International SAT Competitions (2002-2011), http://www.satcompetition.org/
  24. 24.
    Cook, S.A.: The complexity of theorem-proving procedures. In: STOC 1971: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158 (1971)Google Scholar
  25. 25.
    Buning, H.K., Lettman, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press (1999)Google Scholar
  26. 26.
    Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications. In: International Symposium on Multi-Valued Logic, pp. 9–14 (May 2010)Google Scholar
  27. 27.
    Marques-Silva, J., Lynce, I.: On Improving MUS Extraction Algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159–173. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  28. 28.
    Marques-Silva, J., Sakallah, K.: GRASP-a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, pp. 220–227 (November 1996)Google Scholar
  29. 29.
    Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conference, pp. 530–535 (2001)Google Scholar
  30. 30.
    Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  31. 31.
    Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation (4), 75–97 (2008)zbMATHGoogle Scholar
  32. 32.
    Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe Conference, pp. 10880–10885 (March 2003)Google Scholar
  33. 33.
    McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  34. 34.
    Craig, W.: Linear reasoning. A new form of the herbrand-gentzen theorem. Journal of Symbolic Logic 22(3), 250–268 (1957)MathSciNetzbMATHCrossRefGoogle Scholar
  35. 35.
    Pudlak, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62(3), 981–998 (1997)MathSciNetzbMATHCrossRefGoogle Scholar
  36. 36.
    Cheng, L., Chen, D., Wong, M.: DDBDD: Delay-Driven BDD Synthesis for FPGAs. IEEE Transactions on Computer-Aided Design 27(7), 1203–1213 (2008)CrossRefGoogle Scholar
  37. 37.
    Kravets, V., Mishchenko, A.: Sequential logic synthesis using symbolic bi-decomposition. In: Design, Automation and Test in Europe Conference, pp. 1458–1463 (2009)Google Scholar
  38. 38.
    Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification, Release 70930, http://www.eecs.berkeley.edu/~alanmi/abc/
  39. 39.
    Chen, H., Marques-Silva, J.: New and Improved Models for SAT-Based Bi-Decomposition. In: Great Lakes Symposium on VLSI (2012)Google Scholar
  40. 40.
    Chen, M., Mishra, P.: Decision ordering based property decomposition for functional test generation. In: Design Automation and Test in Europe, pp. 167–172 (2011)Google Scholar
  41. 41.
    Chen, H., Marques-Silva, J.: TG-PRO: A SAT-based ATPG System, System Description. Journal on Satisfiability, Boolean Modeling and Computation 8, 83–88 (2012)MathSciNetGoogle Scholar
  42. 42.
    Belov, A., Marques-Silva, J.: Minimally Unsatisfiable Boolean Circuits. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 145–158. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  43. 43.
    Chen, H., Janota, M., Marques-Silva, J.: QBF-Based Boolean Function Bi-Decomposition, Computing Research Repository (CoRR), abs/1112.2313 (December 2011)Google Scholar
  44. 44.
    Chen, H., Janota, M., Marques-Silva, J.: QBF-Based Boolean Function Bi-Decomposition. In: Design Automation and Test in Europe (2012)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2012

Authors and Affiliations

  • Huan Chen
    • 1
  • Joao Marques-Silva
    • 1
  1. 1.Complex & Adaptive Systems Laboratory (CASL) School of Computer Science and Informatics (CSI)University College DublinDublinIreland

Personalised recommendations