Large-Scale Boolean Matching

Chapter

Abstract

In this chapter, we propose a methodology for Boolean matching under permutations of inputs and outputs (PP-equivalence checking problem) – a key step in incremental logic design that identifies large sections of a netlist that are not affected by a change in specifications. When a design undergoes incremental changes, large parts of the circuit may remain unmodified. In these cases, the original and the slightly modified circuits share a number of functionally equivalent subcircuits. Finding and reutilizing the equivalent subcircuits reduce the amount of work in each design iteration and accelerate design closure. In this chapter, we present a combination of fast and effective techniques that can efficiently solve the PP-equivalence checking problem in practice. Our approach integrates graph-based, simulation-driven, and SAT-based techniques to make Boolean matching feasible for large circuits. We verify the validity of our approach on ITC’99 benchmarks. The experimental results confirm scalability of our techniques to circuits with hundreds and even thousands of inputs and outputs.

Keywords

Europe 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdollahi, A.: Signature based Boolean matching in the presence of don’t cares. In: DAC ’08: Proceedings of the 45th annual Design Automation Conference, pp. 642–647. ACM, New York, NY (2008). DOI: http://doi.acm.org/10.1145/1391469.1391635
  2. 2.
    Abdollahi, A., Pedram, M.: A new canonical form for fast Boolean matching in logic synthesis and verification. In: DAC ’05: Proceedings of the 42nd annual Design Automation Conference, pp. 379–384. ACM, New York, NY (2005). DOI: http://doi.acm.org/10.1145/1065579.1065681
  3. 3.
    Agosta, G., Bruschi, F., Pelosi, G., Sciuto, D.: A unified approach to canonical form-based Boolean matching. In: DAC ’07: Proceedings of the 44th annual Design Automation Conference, pp. 841–846. ACM, New York, NY (2007). DOI: http://doi.acm.org/10.1145/1278480.1278689
  4. 4.
    Benini, L., Micheli, G.D.: A survey of Boolean matching techniques for library binding. ACM Transactions on Design Automation of Electronic Systems 2, 193–226 (1997)CrossRefGoogle Scholar
  5. 5.
    Chai, D., Kuehlmann, A.: Building a better Boolean matcher and symmetry detector. In: DATE ’06: Proceedings of the conference on Design, automation and test in Europe, pp. 1079–1084. European Design and Automation Association, 3001 Leuven, Belgium, Belgium (2006)Google Scholar
  6. 6.
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962). DOI: http://doi.acm.org/10.1145/368273.368557
  7. 7.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960). DOI: http://doi.acm.org/10.1145/321033.321034 Google Scholar
  8. 8.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: E. Giunchiglia, A. Tacchella (eds.) SAT, Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer, Heidelberg (2003)Google Scholar
  9. 9.
    Goering, R.: Xilinx ISE handles incremental changes. http://www.eetimes.com/showArticle.jhtml?articleID=196901122 (2009)
  10. 10.
    Krishnaswamy, S., Ren, H., Modi, N., Puri, R.: Deltasyn: An efficient logic difference optimizer for ECO synthesis. In: ICCAD ’09: Proceedings of the 2009 International Conference on Computer-Aided Design, pp. 789–796. ACM, New York, NY (2009). DOI: http://doi.acm.org/10.1145/1687399.1687546
  11. 11.
    Lee, C.C., Jiang, J.H.R., Huang, C.Y.R., Mishchenko, A.: Scalable exploration of functional dependency by interpolation and incremental SAT solving. In: ICCAD ’07: Proceedings of the 2007 IEEE/ACM International Conference on Computer-aided design, pp. 227–233. IEEE Press, Piscataway, NJ (2007)Google Scholar
  12. 12.
    Mishchenko, A.: Logic synthesis and verification group. ABC: A system for sequential synthesis and verification, release 70930. http://www.eecs.berkeley.edu/∼alanmi/abc/ (2008)
  13. 13.
    Mishchenko, A., Chatterjee, S., Brayton, R.: FRAIGs: A unifying representation for logic synthesis and verification. Technical report, UC Berkeley (2005)Google Scholar
  14. 14.
    Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: ICCAD ’06: Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, pp. 836–843. ACM, New York, NY (2006). DOI: http://doi.acm.org/10.1145/1233501.1233679
  15. 15.
    Nocco, S., Stefano, Q.: A probabilistic and approximated approach to circuit-based formal verification. Journal of Satisfiability, Boolean Modeling and Computation 5, 111–132. http://jsat.ewi.tudelft.nl/content/volume5/JSAT5_5_Nocco.pdf (2008)
  16. 16.
    Ray, S., Mishchenko, A., Brayton, R.: Incremental sequential equivalence checking and subgraph isomorphism. In: Proceedings of the International Workshop on Logic Synthesis, pp. 37–42. (2009)Google Scholar
  17. 17.
    Wang, K.H., Chan, C.M., Liu, J.C.: Simulation and SAT-based Boolean matching for large Boolean networks. In: DAC ’09: Proceedings of the 46th Annual Design Automation Conference, pp. 396–401. ACM, New York, NY (2009). DOI: http://doi.acm.org/10.1145/1629911.1630016

Copyright information

© Springer Science+Business Media, LLC 2011

Authors and Affiliations

  1. 1.University of MichiganAnn ArborUSA

Personalised recommendations