Survey on Exact Logic Synthesis Based on Boolean SATisfiability

CHU Zhufei; PAN Hongyang

doi:10.11999/JEIT220391

Volume 45 Issue 1

Jan. 2023

Turn off MathJax

Article Contents

Article Navigation > Journal of Electronics & Information Technology > 2023 > 45(1): 14-23

CHU Zhufei, PAN Hongyang. Survey on Exact Logic Synthesis Based on Boolean SATisfiability[J]. Journal of Electronics & Information Technology, 2023, 45(1): 14-23. doi: 10.11999/JEIT220391

Citation:

CHU Zhufei, PAN Hongyang. Survey on Exact Logic Synthesis Based on Boolean SATisfiability[J]. Journal of Electronics & Information Technology, 2023, 45(1): 14-23. doi: 10.11999/JEIT220391

CHU Zhufei, PAN Hongyang. Survey on Exact Logic Synthesis Based on Boolean SATisfiability[J]. Journal of Electronics & Information Technology, 2023, 45(1): 14-23. doi: 10.11999/JEIT220391

Citation:

CHU Zhufei, PAN Hongyang. Survey on Exact Logic Synthesis Based on Boolean SATisfiability[J]. Journal of Electronics & Information Technology, 2023, 45(1): 14-23. doi: 10.11999/JEIT220391

PDF( 1926 KB)

Survey on Exact Logic Synthesis Based on Boolean SATisfiability

doi: 10.11999/JEIT220391

CHU Zhufei^,,
PAN Hongyang

Faculty of Electrical Engineering and Computer Science (EECS), Ningbo University, Ningbo 315211, China

Funds: The National Natural Science Foundation of China (61871242), The Open research fund of State Key Laboratory of Application Specific Integrated Circuits and Systems (2021KF008)

Received Date: 2022-04-02
Rev Recd Date: 2022-08-29

Available Online: 2022-09-01

Publish Date: 2023-01-17

Abstract

Abstract

Logic synthesis is a critical step in the Electronic Design Automation(EDA). Traditional global heuristic-based logic synthesis has many challenges as computing power keeps increasing and new computing paradigms emerge. There is a problem with heuristic algorithm in a suboptimal solution. As computing power improving, logic optimization is increasingly pursuing exact solutions rather than suboptimal solutions. First, the logic representations and the Boolean SATisfiability(SAT) problem are briefly described. Then, the research progress of exact synthesis in area optimization and depth optimization of Boolean logic network at two aspects, exact synthesis algorithm and encoding, are introduced. Finally, the future trends in exact synthesis are discussed.
- Logic synthesis,
- Exact synthesis,
- Boolean SATisfiability (SAT),
- Majority logic

FullText(HTML)

References(31)

References

[1]	HAASWIJK W J. SAT-based exact synthesis for multi-level logic networks[D]. EPFL, 2019.
[2]	KNUTH D E. The Art of Computer Programming[M]. Upper Saddle River: Addison-Wesley Professional, 2005.
[3]	HAASWIJK W, SOEKEN M, MISHCHENKO A, et al. SAT-based exact synthesis: Encodings, topology families, and parallelism[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 39(4): 871–884. doi: 10.1109/TCAD.2019.2897703
[4]	QUINE W V. The problem of simplifying truth functions[J]. The American Mathematical Monthly, 1952, 59(8): 521–531. doi: 10.1080/00029890.1952.11988183
[5]	ERNST E A. Optimal combinational multi-level logic synthesis[D]. [Ph. D. dissertation], The University of Michigan, 2009.
[6]	EÉN N. Practical SAT-a tutorial on applied satisfiability solving[R]. 2007.
[7]	SOEKEN M, AMARÙ L, GAILLARDON P E, et al. Exact synthesis of majority-inverter graphs and its applications[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2017, 36(11): 1842–1855. doi: 10.1109/TCAD.2017.2664059
[8]	CHU Zhufei, SOEKEN M, XIA Yinshui, et al. Advanced functional decomposition using majority and its applications[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 39(8): 1621–1634. doi: 10.1109/TCAD.2019.2925392
[9]	HAASWIJK W, SOEKEN M, MISHCHENKO A, et al. SAT based exact synthesis using DAG topology families[C]. The 55Th ACM/ESDA/IEEE Design Automation Conference (DAC), San Francisco, USA, 2018: 1–6.
[10]	HAASWIJK W J, SOEKEN M, AMARU L, et al. LUT mapping and optimization for majority-inverter graphs[C]. The 25th International Workshop on Logic & Synthesis (IWLS), Austin, USA, 2016.
[11]	HAASWIJK W, SOEKEN M, AMARÙ L, et al. A novel basis for logic rewriting[C]. 2017 22nd Asia and South Pacific Design Automation Conference (ASP-DAC), Chiba, Japan, 2017: 151–156.
[12]	CHU Zhufei, HAASWIJK W, SOEKEN M, et al. Exact synthesis of Boolean functions in majority-of-five forms[C]. 2019 IEEE International Symposium on Circuits and Systems (ISCAS), Sapporo, Japan, 2019: 1–5.
[13]	MARAKKALAGE D S, TESTA E, RIENER H, et al. Three-input gates for logic synthesis[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2021, 40(10): 2184–2188. doi: 10.1109/TCAD.2020.3032625
[14]	HAASWIJK W, TESTA E, SOEKEN M, et al. Classifying functions with exact synthesis[C]. 2017 IEEE 47th International Symposium on Multiple-Valued Logic (ISMVL), Novi Sad, Serbia, 2017: 272–277.
[15]	PETKOVSKA A, SOEKEN M, DE MICHELI G, et al. Fast hierarchical NPN classification[C]. 2016 26th International Conference on Field Programmable Logic and Applications (FPL), Lausanne, Switzerland, 2016: 1–4.
[16]	HUANG Zheng, WANG Lingli, NASIKOVSKIY Y, et al. Fast Boolean matching based on NPN classification[C]. 2013 International Conference on Field-Programmable Technology (FPT), Kyoto, Japan, 2013: 310–313.
[17]	ZHOU Xuegong, WANG Lingli, and MISHCHENKO A. Fast exact NPN classification by Co-designing canonical form and its computation algorithm[J]. IEEE Transactions on Computers, 2020, 69(9): 1293–1307. doi: 10.1109/TC.2020.2971466
[18]	SOEKEN M, DE MICHELI G, and MISHCHENKO A. Busy man's synthesis: Combinational delay optimization with SAT[C]. 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE), Lausanne, Switzerland, 2017: 830–835.
[19]	SOEKEN M, HAASWIJK W, TESTA E, et al. Practical exact synthesis[C]. 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), Dresden, Germany, 2018: 309–314.
[20]	RIENER H, HAASWIJK W, MISHCHENKO A, et al. On-the-fly and DAG-aware: Rewriting Boolean networks with exact synthesis[C]. 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), Florence, Italy, 2019: 1649–1654.
[21]	RIENER H, MISHCHENKO A, and SOEKEN M. Exact DAG-aware rewriting[C]. 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE), Grenoble, France, 2020: 732–737.
[22]	GROßE D, WILLE R, DUECK G W, et al. Exact multiple-control Toffoli network synthesis with SAT techniques[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2009, 28(5): 703–715. doi: 10.1109/TCAD.2009.2017215
[23]	WILLE R, SOEKEN M, PRZIGODA N, et al. Exact synthesis of Toffoli gate circuits with negative control lines[C]. The 2012 IEEE 42nd International Symposium on Multiple-Valued Logic, Victoria, Canada, 2012: 69–74.
[24]	KOLE A, RANI P M N, DATTA K, et al. Exact synthesis of ternary reversible functions using ternary Toffoli gates[C]. 2017 IEEE 47th International Symposium on Multiple-Valued Logic (ISMVL), Novi Sad, Serbia, 2017: 179–184.
[25]	RIENER H, EHLERS R, DE O SCHMITT B, et al. Exact synthesis of ESOP forms[M]. DRECHSLER R and SOEKEN M. Advanced Boolean Techniques: Selected Papers from the 13th International Workshop on Boolean Problems. Cham: Springer, 2020: 177–194.
[26]	WANG Xuan, CHU Zhufei, and QIAN Weikang. MinSC: An exact synthesis-based method for minimal-area stochastic circuits under relaxed error bound[C]. 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), Munich, Germany, 2021: 1–9.
[27]	HE Xiang and CHU Zhufei. Stochastic circuit synthesis via satisfiability[J]. Integration, 2022, 84: 84–91. doi: 10.1016/J.VLSI.2021.11.003
[28]	CHEN Lin and CHU Zhufei. Towards optimal logic representations for implication-based memristive circuits[C]. 2020 China Semiconductor Technology International Conference (CSTIC), Shanghai, China, 2020: 1–3.
[29]	PAN Hongyang and CHU Zhufei. A semi-tensor product based SAT all solutions solver[C]. The 2021 CCF Integrated Circuit Design and Automation Conference (CCFDAC), Wuhan, China, 2020.
[30]	ZHANG Heteng, JIANG J H R, and MISHCHENKO A. A circuit-based SAT solver for logic synthesis[C]. 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), Munich, Germany, 2021: 1–6.
[31]	HOSNY A, HASHEMI S, SHALAN M, et al. DRiLLS: Deep reinforcement learning for logic synthesis[C]. 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC), Beijing, China, 2020: 581–586.