Survey on Exact Logic Synthesis Based on Boolean SATisfiability
-
摘要: 逻辑综合是电子设计自动化(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.
-
Key words:
- Logic synthesis /
- Exact synthesis /
- Boolean SATisfiability (SAT) /
- Majority logic
-
[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. 期刊类型引用(12)
1. 张艳睛，龙伟军，潘明海. 射频辐射源的高精度参数估计. 现代电子技术. 2022(15): 63-68 . 
百度学术2. 陈万里，李伟，柴远波. 一种低信噪比下的LFM脉冲信号起始频率校正方法. 火力与指挥控制. 2021(02): 58-63 . 百度学术3. 孙同晶，刘桐，杨阳. 多阶次分数阶傅里叶域特征融合的主动声呐目标稀疏表示分类方法. 电子与信息学报. 2021(03): 809-816 . 
本站查看4. 李亚利，刘佳. 基于非平稳信号时频分析的DDoS攻击检测仿真. 计算机仿真. 2021(05): 353-356+370 . 百度学术5. 张玉，李天琪，张进，唐波. 基于集成固有时间尺度分解的IFF辐射源个体识别算法. 电子与信息学报. 2020(02): 430-437 . 本站查看6. 邬俊阳，陈欣. 基于迭代搜索的线性调频脉冲信号参数估计方法. 探测与控制学报. 2020(04): 39-46 . 百度学术7. 林江刚，胡正新，李晶，翟怡萌，邓艾东. 低转速下基于AE信号与LMD的滚动轴承故障诊断. 动力工程学报. 2019(04): 293-298 . 百度学术8. 刘会杰，高新海，郭汝江. 一种低副瓣无混叠的线性调频信号时频分析方法. 电子与信息学报. 2019(11): 2614-2622 . 本站查看9. 林江刚，胡正新，李晶，翟怡萌，邓艾东. 基于AE信号与VMD的滚动轴承故障诊断研究. 燃气轮机技术. 2018(03): 34-38 . 百度学术10. 欧国建，张淑芳，邓剑勋，蒋清平. 利用FFT实现对LFM信号的快速稀疏分解. 数据采集与处理. 2018(05): 865-871 . 百度学术11. 孙湘，华钢. 生物特征信号提纯算法的设计与实现. 生物医学工程研究. 2018(04): 492-495 . 百度学术12. 陈小龙，关键，黄勇，于晓涵，刘宁波，董云龙，何友. 雷达低可观测动目标精细化处理及应用. 科技导报. 2017(20): 19-27 . 百度学术其他类型引用(12)
-
下载:
百度学术
图(5)
计量
- 文章访问数: 1434
- HTML全文浏览量: 1056
- PDF下载量: 264
- 被引次数: 24
下载:
