高级搜索

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

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

储著飞 潘鸿洋

储著飞, 潘鸿洋. 基于布尔可满足性的精确逻辑综合综述[J]. 电子与信息学报, 2023, 45(1): 14-23. doi: 10.11999/JEIT220391
引用本文: 储著飞, 潘鸿洋. 基于布尔可满足性的精确逻辑综合综述[J]. 电子与信息学报, 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

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

doi: 10.11999/JEIT220391
基金项目: 国家自然科学基金(61871242),专用集成电路与系统国家重点实验室开放研究课题基金(2021KF008)
详细信息
    作者简介:

    储著飞:男,副教授,博士生导师,研究方向为逻辑综合与优化

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

    通讯作者:

    储著飞 chuzhufei@nbu.edu.cn

  • 中图分类号: TN47

Survey on Exact Logic Synthesis Based on Boolean SATisfiability

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)问题;其次针对精确综合的算法、编码等方面介绍了在布尔逻辑网络的面积优化和深度优化方面的精确综合研究进展;最后对精确综合的未来发展趋势进行讨论。
  • 图  1  布尔链示意图

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

    图  3  围栏结构

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

    图  5  NPN结构

  • [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.
  • 加载中
图(5)
计量
  • 文章访问数:  188
  • HTML全文浏览量:  137
  • PDF下载量:  48
  • 被引次数: 0
出版历程
  • 收稿日期:  2022-04-02
  • 修回日期:  2022-08-29
  • 网络出版日期:  2022-09-01
  • 刊出日期:  2023-01-17

目录

    /

    返回文章
    返回