基于布尔可满足性的精确逻辑综合综述

储著飞; 潘鸿洋

doi:10.11999/JEIT220391

基于布尔可满足性的精确逻辑综合综述

doi: 10.11999/JEIT220391

储著飞^,,
潘鸿洋

宁波大学信息科学与工程学院宁波 315211

基金项目: 国家自然科学基金(61871242)，专用集成电路与系统国家重点实验室开放研究课题基金(2021KF008)

详细信息

作者简介:
储著飞：男，副教授，博士生导师，研究方向为逻辑综合与优化

潘鸿洋：男，硕士生，研究方向为逻辑综合与优化

通讯作者:
储著飞　chuzhufei@nbu.edu.cn

中图分类号: TN47
计量
- 文章访问数: 896
- HTML全文浏览量: 681
- PDF下载量: 216
- 被引次数: 0
出版历程
- 收稿日期: 2022-04-02
- 修回日期: 2022-08-29
- 网络出版日期: 2022-09-01
- 刊出日期: 2023-01-17

Survey on Exact Logic Synthesis Based on Boolean SATisfiability

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)

摘要

摘要: 逻辑综合是电子设计自动化(EDA)的重要步骤，随着算力逐渐提升和新的计算范式不断涌现，传统基于全局启发式算法的逻辑综合面临新的挑战。启发式算法面临的主要问题是得到一个次优解，随着算力的提升，逻辑优化越来越追求精确解而不满足于次优解。该文首先简述逻辑函数表达方法和布尔可满足性(SAT)问题；其次针对精确综合的算法、编码等方面介绍了在布尔逻辑网络的面积优化和深度优化方面的精确综合研究进展；最后对精确综合的未来发展趋势进行讨论。
- 逻辑综合 /
- 精确综合 /
- 布尔可满足性 /
- 多数逻辑门
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

HTML全文

图 1 布尔链示意图

下载: 全尺寸图片幻灯片

图 2 基于SAT的精确综合流程图

下载: 全尺寸图片幻灯片

图 3 围栏结构

下载: 全尺寸图片幻灯片

图 4 全加器逻辑网络的不同多数逻辑表达

下载: 全尺寸图片幻灯片

图 5 NPN结构

下载: 全尺寸图片幻灯片

参考文献(31)

[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.