Document Open Access Logo

eSLIM: Circuit Minimization with SAT Based Local Improvement

Authors Franz-Xaver Reichl , Friedrich Slivovsky , Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.23.pdf
  • Filesize: 0.92 MB
  • 14 pages

Document Identifiers

Author Details

Franz-Xaver Reichl
  • TU Wien, Austria
Friedrich Slivovsky
  • University of Liverpool, UK
Stefan Szeider
  • TU Wien, Austria

Funding

This work was supported by the Vienna Science and Technology Fund (WWTF) under grant 10.47379/ICT19060, and the Austrian Science Fund (FWF) under grants 10.55776/W1255 and 10.55776/P36420.

Acknowledgements

The authors thank Alan Mishchenko for suggesting to represent local synthesis tasks with Boolean relations.

Cite AsGet BibTex

Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. eSLIM: Circuit Minimization with SAT Based Local Improvement. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 23:1-23:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.23

Abstract

eSLIM is a tool for circuit minimization that utilizes Exact Synthesis and the SAT-based local improvement method (SLIM) to locally improve circuits. eSLIM improves upon the earlier prototype CIOPS that uses Quantified Boolean Formulas (QBF) to succinctly encode resynthesis of multi-output subcircuits subject to don't cares. This paper describes two improvements. First, it presents a purely propositional encoding based on a Boolean relation characterizing the input-output behavior of the subcircuit under don't cares. This allows the use of a SAT solver for resynthesis, substantially reducing running times when applied to functions from the IWLS 2023 competition, where eSLIM placed second. Second, it proposes circuit partitioning techniques in which don't cares for a subcircuit are captured only with respect to an enclosing window, rather than the entire circuit. Circuit partitioning trades completeness for efficiency, and successfully enables the application of exact synthesis to some of the largest circuits in the EPFL suite, leading to improvements over the current best implementation for several instances.

Subject Classification

ACM Subject Classification
  • Hardware → Circuit optimization
  • Theory of computation → Automated reasoning
Keywords
  • QBF
  • Exact Synthesis
  • Circuit Minimization
  • SLIM

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Luca Amarú, Pierre-Emmanuel Gaillardon, and Giovanni De Micheli. The EPFL combinational benchmark suite. In International Workshop on Logic & Synthesis (IWLS), 2015. URL: https://github.com/lsils/benchmarks.
  2. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified Boolean formulas. In Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. Google Scholar
  3. Armin Biere. The AIGER And-Inverter Graph (AIG) format version 20071012. Technical Report 07/1, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2007. Google Scholar
  4. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  5. Armin Biere, Keijo Heljanko, and Siert Wieringa. AIGER 1.9 and beyond. Technical Report 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2011. Google Scholar
  6. Robert K. Brayton, Gary D. Hachtel, and Alberto L. Sangiovanni-Vincentelli. Multilevel logic synthesis. Proc. IEEE, 78(2):264-300, 1990. Google Scholar
  7. Robert K. Brayton and Alan Mishchenko. ABC: An academic industrial-strength verification tool. In CAV, volume 6174 of LNCS, pages 24-40. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_5.
  8. Huan Chen, Mikolás Janota, and João Marques-Silva. QBF-based Boolean function bi-decomposition. In DATE, pages 816-819. IEEE, 2012. URL: https://doi.org/10.1109/DATE.2012.6176606.
  9. Andrea Costamagna, Alan Mishchenko, and Giovanni De Micheli. The combinational-complexity game for symmetric functions. In IWLS, 2023. URL: https://si2.epfl.ch/~demichel/publications/archive/2023/AC.pdf.
  10. Giovanni De Micheli. Synthesis and Optimization of Digital Circuits. McGraw Hill, 1994. Google Scholar
  11. Johannes K. Fichte, Neha Lodha, and Stefan Szeider. SAT-based local improvement for finding tree decompositions of small width. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of LNCS, pages 401-411. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_25.
  12. Masahiro Fujita. Toward unification of synthesis and verification in topologically constrained logic design. Proc. IEEE, 103(11):2052-2060, 2015. URL: https://doi.org/10.1109/JPROC.2015.2476472.
  13. Masahiro Fujita, Satoshi Jo, Shohei Ono, and Takeshi Matsumoto. Partial synthesis through sampling with and without specification. In ICCAD, pages 787-794. IEEE, 2013. URL: https://doi.org/10.1109/ICCAD.2013.6691203.
  14. Masahiro Fujita, Yusuke Kimura, Xingming Le, Yukio Miyasaka, and Amir Masoud Gharehbaghi. Synthesis and optimization of multiple portions of circuits for ECO based on set-covering and QBF formulations. In DATE, pages 744-749. IEEE, 2020. URL: https://doi.org/10.23919/DATE48585.2020.9116459.
  15. Dale Gai. TSMC price hike indicates capacity tightness to persist in 2022, may hit smartphone shipments. online, 2021. URL: https://www.counterpointresearch.com/insights/tsmc-price-hike/.
  16. Winston Haaswijk, Mathias Soeken, Alan Mishchenko, and Giovanni De Micheli. SAT-based exact synthesis: Encodings, topology families, and parallelism. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 39(4):871-884, 2020. URL: https://doi.org/10.1109/TCAD.2019.2897703.
  17. Rahul Ilango, Bruno Loff, and Igor C. Oliveira. NP-hardness of circuit minimization for multi-output functions. In Shubhangi Saraf, editor, CCC, volume 169 of LIPIcs, pages 22:1-22:36. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.CCC.2020.22.
  18. Mikolás Janota. Towards generalization in QBF solving via machine learning. In AAAI, pages 6607-6614. AAAI Press, 2018. URL: https://doi.org/10.1609/AAAI.V32I1.12208.
  19. Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artif. Intell., 234:1-25, 2016. URL: https://doi.org/10.1016/j.artint.2016.01.004.
  20. Donald Ervin Knuth. The Art of Computer Programming. Volume 4A, Combinatorial Algorithms, Part 1. Addison Wesley, 1st edition. edition, 2011. Google Scholar
  21. Arist Kojevnikov, Alexander S. Kulikov, and Grigory Yaroslavtsev. Finding efficient circuits using SAT-solvers. In SAT, volume 5584 of LNCS, pages 32-44. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_5.
  22. Alexander S. Kulikov, Danila Pechenev, and Nikita Slezkin. SAT-based circuit local improvement. In MFCS, volume 241 of LIPIcs, pages 67:1-67:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.67.
  23. Tung-Yuan Lee, Chia-Cheng Wu, Chia-Chun Lin, Yung-Chih Chen, and Chun-Yao Wang. Logic optimization with considering Boolean relations. In 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 761-766. IEEE, 2018. URL: https://doi.org/10.23919/DATE.2018.8342109.
  24. Neha Lodha, Sebastian Ordyniak, and Stefan Szeider. A SAT approach to branchwidth. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of LNCS, pages 179-195. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_12.
  25. Alan Mishchenko and Robert K. Brayton. SAT-based complete don't-care computation for network optimization. In DATE, pages 412-417. IEEE Computer Society, 2005. Google Scholar
  26. Alan Mishchenko, Robert K. Brayton, Jie-Hong R. Jiang, and Stephen Jang. Scalable don't-care-based logic optimization and resynthesis. ACM Trans. Reconfigurable Technol. Syst., 4(4):34:1-34:23, 2011. URL: https://doi.org/10.1145/2068716.2068720.
  27. Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Turbocharging treewidth-bounded Bayesian network structure learning. In Proceeding of AAAI-21, the Thirty-Fifth AAAI Conference on Artificial Intelligence, pages 3895-3903. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16508.
  28. Kavita Ravi and Fabio Somenzi. Minimal assignments for bounded model checking. In Kurt Jensen and Andreas Podelski, editors, TACAS, volume 2988 of Lecture Notes in Computer Science, pages 31-45. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24730-2_3.
  29. Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. eSLIM. Software, This work was supported by the Vienna Science and Technology Fund (WWTF) under grant 10.47379/ICT19060, and the Austrian Science Fund (FWF) under grant 10.55776/W1255., swhId: https://archive.softwareheritage.org/swh:1:dir:9d2862aedfe458cfb06d4d43da6c0f46ed578c91;origin=https://github.com/fxreichl/eSLIM;visit=swh:1:snp:ebfe92c3c6e3f45b9d69b59b4a1873264e9dcebd;anchor=swh:1:rev:779e64b93465754590fc1321d595ed48c8e39587 (visited on 2024-08-05). URL: https://github.com/fxreichl/eSLIM.
  30. Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. Circuit minimization with QBF-based exact synthesis. In AAAI. AAAI Press, 2023. URL: https://doi.org/10.1609/AAAI.V37I4.25524.
  31. Heinz Riener, Winston Haaswijk, Alan Mishchenko, Giovanni De Micheli, and Mathias Soeken. On-the-fly and DAG-aware: Rewriting Boolean networks with exact synthesis. In DATE, pages 1649-1654. IEEE, 2019. URL: https://doi.org/10.23919/DATE.2019.8715185.
  32. Heinz Riener, Alan Mishchenko, and Mathias Soeken. Exact dag-aware rewriting. In DATE, pages 732-737. IEEE, 2020. URL: https://doi.org/10.23919/DATE48585.2020.9116379.
  33. Hamid Savoj and Robert K. Brayton. The use of observability and external don't cares for the simplification of multi-level networks. In DAC, pages 297-301. IEEE Computer Society Press, 1990. Google Scholar
  34. Andre Schidler and Stefan Szeider. SAT-boosted tabu search for coloring massive graphs. J. Exp. Algorithmics, 2825(1.5):1-19, 2023. URL: https://doi.org/10.1145/3603112.
  35. André Schidler and Stefan Szeider. SAT-based decision tree learning for large data sets. J. Artificial Intelligence Research, 2024. To appear. Google Scholar
  36. André Schidler and Stefan Szeider. Structure-guided local improvement for maximum satisfiability. In Peter Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Catalonia, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. To appear. Google Scholar
  37. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In ICTAI, pages 78-84. IEEE, 2019. Google Scholar
  38. Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Peter van Beek, editor, CP, volume 3709 of LNCS, pages 827-831. Springer, 2005. URL: https://doi.org/10.1007/11564751_73.
  39. Eleonora Testa, Luca G. Amarù, Mathias Soeken, Alan Mishchenko, Patrick Vuillod, Pierre-Emmanuel Gaillardon, and Giovanni De Micheli. Extending Boolean methods for scalable logic synthesis. IEEE Access, 8:226828-226844, 2020. URL: https://doi.org/10.1109/ACCESS.2020.3045014.
  40. University of California Berkeley. Berkeley logic interchange format (BLIF), 1992. URL: https://course.ece.cmu.edu/~ee760/760docs/blif.pdf.
  41. Robert Wille, Hoang Minh Le, Gerhard W. Dueck, and Daniel Große. Quantified synthesis of reversible logic. In DATE, pages 1015-1020. ACM, 2008. URL: https://doi.org/10.1109/DATE.2008.4484814.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact