基于半张量积的逻辑综合研究进展

储著飞; 马铖昱; 闫鸣; 潘家祥; 潘鸿洋; 王伦耀; 夏银水

doi:10.11999/JEIT231457

基于半张量积的逻辑综合研究进展

doi: 10.11999/JEIT231457

1.
宁波大学信息科学与工程学院宁波 315211
2.
复旦大学微电子学院上海 200433

基金项目: 国家自然科学基金(62274100, U23A20351)，浙江省重点研发计划(2024C01111)，宁波市重点研发计划(2023Z071)

详细信息

作者简介:
储著飞：男，教授，研究方向为集成电路电子设计自动化，逻辑综合

马铖昱：男，硕士生，研究方向为集成电路电子设计自动化，逻辑综合

闫鸣：男，硕士生，研究方向为集成电路电子设计自动化，逻辑综合

潘家祥：男，硕士生，研究方向为集成电路电子设计自动化，逻辑综合

潘鸿洋：男，硕士生，研究方向为集成电路电子设计自动化，逻辑综合

王伦耀：男，教授，研究方向为集成电路电子设计自动化，逻辑综合

夏银水：男，教授，研究方向为集成电路电子设计自动化，集成电路设计

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

中图分类号: TN47
计量
- 文章访问数: 94
- HTML全文浏览量: 38
- PDF下载量: 19
- 被引次数: 0
出版历程
- 收稿日期: 2024-01-09
- 修回日期: 2024-03-15
- 网络出版日期: 2024-03-21

Research Progress in Logic Synthesis Based on Semi-Tensor Product

1.
Faculty of Electrical Engineering and Computer Science (EECS), Ningbo University, Ningbo 315211, China
2.
School of Microelectronics, Fudan University, Shanghai 200433, China

Funds: The National Natural Science Foundation of China (62274100, U23A20351), The Key R&D Program of Zhejiang Province (2024C01111), The Key R&D Program of Ningbo City (2023Z071)

摘要

摘要: 逻辑综合在现代电子设计自动化流程中扮演着至关重要的角色。随着计算能力的不断增强以及新的计算范式的涌现，各种高效的布尔可满足性(SAT)求解器和电路仿真器(Simulator)得以开发，并在逻辑综合的领域取得了显著的应用。该文首先对布尔可满足性问题和电路逻辑仿真器进行了简要介绍；其次回顾了矩阵半张量积的发展历程，并根据半张量积的基本原理深入阐述了其在推理引擎和逻辑综合方面的研究进展；最后，对未来可能对逻辑综合产生重大影响的新技术进行了展望。
- 逻辑综合 /
- 逻辑优化 /
- 推理引擎 /
- 半张量积
Abstract: Logic synthesis plays a crucial role in the modern electronic design automation process. With the continuous enhancement of computational capabilities and the emergence of new computing paradigms, various efficient Boolean SATisfiability (SAT) solvers and circuit simulators have been developed and applied in the context of logic synthesis. First, the overview of the Boolean Satisfiability problem and circuit logic simulator is briefly described. Subsequently, the historical development of the matrix semi-tensor product is reviewed, and based on the fundamental principles of the semi-tensor product, its research progress in inference engines and logic synthesis is expounded. Finally, a prospective analysis is conducted on emerging technologies that may significantly impact logic synthesis in the future.
- Logic synthesis /
- Logic optimization /
- Reasoning engine /
- Semi-Tensor Product(STP)

HTML全文

图 1 逻辑网络转换成真值表形式

下载: 全尺寸图片幻灯片

图 2 电路节点真值表

下载: 全尺寸图片幻灯片

图 3 评估插入替换项的示例

下载: 全尺寸图片幻灯片

图 4 SAT Sweeping 框架

下载: 全尺寸图片幻灯片

图 5 验证过程图

下载: 全尺寸图片幻灯片

图 6 对应的4-LUTs网络

下载: 全尺寸图片幻灯片

参考文献(68)

[1]	储著飞, 潘鸿洋. 基于布尔可满足性的精确逻辑综合综述[J]. 电子与信息学报, 2023, 45(1): 14–23. doi: 10.11999/JEIT220391. CHU Zhufei and PAN Hongxiang. Survey on exact logic synthesis based on boolean SATisfiability[J]. Journal of Electronics & Information Technology, 2023, 45(1): 14–23. doi: 10.11999/JEIT220391.
[2]	PAN Hongyang and CHU Zhufei. A semi-tensor product based all solutions boolean satisfiability solver[J]. Journal of Computer Science and Technology, 2023, 38(3): 702–713. doi: 10.1007/s11390-022-1981-4.
[3]	ZHANG Ruibing, PAN Hongyang, and CHU Zhufei. Logic circuit simulation based on semi-tensor product[C]. Proceedings of 2023 China Semiconductor Technology International Conference, Shanghai, China, 2023: 1–3. doi: 10.1109/CSTIC58779.2023.10219157.
[4]	FROLEYKS N, HEULE M, ISER M, et al. SAT competition 2020[J]. Artificial Intelligence, 2021, 301: 103572. doi: 10.1016/j.artint.2021.103572.
[5]	NADEL A. Introducing intel(R) SAT solver[C]. The 25th International Conference on Theory and Applications of Satisfiability Testing, Haifa, Israel, 2022: 8: 1–8: 23. doi: 10.4230/LIPIcs.SAT.2022.8.
[6]	LEE S Y, RIENER H, MISHCHENKO A, et al. A simulation-guided paradigm for logic synthesis and verification[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022, 41(8): 2573–2586. doi: 10.1109/TCAD.2021.3108704.
[7]	MAGYARI A and CHEN Yuhua. Review of state-of-the-art FPGA applications in IoT networks[J]. Sensors, 2022, 22(19): 7496. doi: 10.3390/s22197496.
[8]	CHENG Daizhan. Semi-tensor product of matrices and its application to Morgen’s problem[J]. Science in China Series:Information Sciences, 2001, 44(3): 195–212. doi: 10.1007/bf02714570.
[9]	CHENG Daizhan. Matrix and Polynomial Approach to Dynamic Control Systems[M]. Beijing: Science Press, 2002.
[10]	程代展, 齐洪胜. 矩阵的半张量积理论与应用[M]. 北京: 科学出版社, 2007. CHENG Daizhan and QI Hongsheng. Semi-Tensor Product of Matrices—Theory and Applications[M]. Beijing: Science Press, 2007.
[11]	CHU Zhufei. Semi-tensor product (STP) engine for electronic design automation (EDA)[EB/OL]. https://gitee.com/zfchu/stp, 2023.
[12]	CHENG Daizhan, QI Hongsheng, and ZHAO Yin. An Introduction to semi-Tensor Product of Matrices and its Applications[M]. Singapore: World Scientific, 2012.
[13]	VAN LOAN C F. The ubiquitous Kronecker product[J]. Journal of Computational and Applied Mathematics, 2000, 123(1/2): 85–100. doi: 10.1016/S0377-0427(00)00393-9.
[14]	程代展, 齐洪胜, 赵寅. 布尔网络的分析与控制—矩阵半张量积方法[J]. 自动化学报, 2011, 37(5): 529–540. doi: 10.3724/SP.J.1004.2011.00529. CHENG Daizhan, QI Hongsheng, and ZHAO Yin. Analysis and control of boolean networks: A semi-tensor product approach[J]. Acta Automatica Sinica, 2011, 37(5): 529–540. doi: 10.3724/SP.J.1004.2011.00529.
[15]	HORN R A and JOHNSON C R. Matrix Analysis[M]. 2nd ed. Cambridge: Cambridge University Press, 2012.
[16]	RÅDE L and WESTERGREN B. Mathematics Handbook for Science and Engineering[M]. 4th ed. Berlin: Springer, 1999. doi: 10.1007/978-3-662-03556-6.
[17]	CHENG Daizhan. On logic-based intelligent systems[C]. 2005 International Conference on Control and Automation, Budapest, Hungary, 2005: 71–76. doi: 10.1109/ICCA.2005.1528094.
[18]	CHENG Daizhan and QI Hongsheng. Matrix expression of logic and fuzzy control[C]. The 44th IEEE Conference on Decision and Control, Seville, Spain, 2005: 3273–3278. doi: 10.1109/CDC.2005.1582666.
[19]	KHATRI C G and RAO C R. Solutions to some functional equations and their applications to characterization of probability distributions[J]. Sankhyā: The Indian Journal of Statistics, Series A, 1968, 30(2): 167–180.
[20]	ZHANG Xiao, MENG Min, WANG Yuanhua, et al. Criteria for observability and reconstructibility of Boolean control networks via set controllability[J]. IEEE Transactions on Circuits and Systems II:Express Briefs, 2021, 68(4): 1263–1267. doi: 10.1109/TCSII.2020.3021190.
[21]	ZHANG Xiao, WANG Yuanhua, and CHENG Daizhan. Incomplete logical control system and its application to some intellectual problems[J]. Asian Journal of Control, 2018, 20(2): 697–706. doi: 10.1002/asjc.1579.
[22]	CHENG Daizhan, WU Yuhu, ZHAO Guodong, et al. A comprehensive survey on STP approach to finite games[J]. Journal of Systems Science and Complexity, 2021, 34(5): 1666–1680. doi: 10.1007/s11424-021-1232-8.
[23]	MARDEN J R, ARSLAN G, and SHAMMA J S. Cooperative control and potential games[J]. IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), 2009, 39(6): 1393–1407. doi: 10.1109/TSMCB.2009.2017273.
[24]	LI Rui and CHU Tianguang. Synchronization in an array of coupled Boolean networks[J]. Physics Letters A, 2012, 376(45): 3071–3075. doi: 10.1016/j.physleta.2012.08.037.
[25]	EÉN N and SÖRENSSON N. An extensible SAT-solver[C]. The 6th International Conference on Theory and Applications of Satisfiability Testing, Santa Margherita Ligure, Italy, 2003: 502–518. doi: 10.1007/978-3-540-24605-3_37.
[26]	DAVIS M, LOGEMANN G, and LOVELAND D. A machine program for theorem-proving[J]. Communications of the ACM, 1962, 5(7): 394–397. doi: 10.1145/368273.368557.
[27]	MARQUES-SILVA J, LYNCE I, and MALIK S. Conflict-driven clause learning SAT solvers[M]. BIERE A, HEULE M, VAN MAAREN H, et al. Handbook of Satisfiability. 2nd ed. Amsterdam: IOS Press, 2021: 133–182.
[28]	CABODI G, CAMURATI P E, PALENA M, et al. Interpolation with guided refinement: Revisiting incrementality in SAT-based unbounded model checking[J]. Formal Methods in System Design, 2022, 60(2): 117–146. doi: 10.1007/s10703-022-00406-Proceedings of the. doi: 10.1007/s10703-022-00406-Proceedingsofthe.
[29]	SUNHARE P, CHOWDHARY R R, and CHATTOPADHYAY M K. Internet of things and data mining: An application oriented survey[J]. Journal of King Saud University-Computer and Information Sciences, 2022, 34(6): 3569–3590. doi: 10.1016/j.jksuci.2020.07.002.
[30]	ZHANG Yueling, PU Geguang, and SUN Jun. Accelerating All-SAT computation with short blocking clauses[C]. The 35th IEEE/ACM International Conference on Automated Software Engineering, Melbourne, Australia, 2020: 6–17.
[31]	TODA T and SOH T. Implementing efficient all solutions SAT solvers[J]. ACM Journal of Experimental Algorithmics, 2016, 21(1.12): 1–44. doi: 10.1145/2975585.
[32]	YU Yinlei, SUBRAMANYAN P, TSISKARIDZE N, et al. All-SAT using minimal blocking clauses[C]. 2014 27th International Conference on VLSI Design and 2014 13th International Conference on Embedded Systems, Mumbai, India, 2014: 86–91. doi: 10.1109/VLSID.2014.22.
[33]	FRIED D, NADEL A, and SHALMON Y. AllSAT for combinational circuits[C]. The 26th International Conference on Theory and Applications of Satisfiability Testing, Alghero, Italy, 2023: 9: 1–9: 18. doi: 10.4230/LIPIcs.SAT.2023.9.
[34]	PAN Hongyang and CHU Zhufei. A semi-tensor product based all solutions boolean satisfiability solver[C]. 2021 CCF Integrated Circuit Design and Automation Conference, Wuhan, China, 2020.
[35]	MASINA G, SPALLITTA G, and SEBASTIANI R. On CNF conversion for disjoint SAT enumeration[C]. The 26th International Conference on Theory and Applications of Satisfiability Testing, Alghero, Italy, 2023: 15: 1–15: 16. doi: 10.4230/LIPIcs.SAT.2023.15.
[36]	CAI Shaowei and ZHANG Xindi. Deep cooperation of cdcl and local search for sat[C]. The 24th International Conference on Theory and Applications of Satisfiability Testing, Barcelona, Spain, 2021: 64–81. doi: 10.1007/978-3-030-80223-3_6.
[37]	KULIKOV A S, PECHENEV D, and SLEZKIN N. SAT-based circuit local improvement[J]. arXiv: 2102.12579, 2021.
[38]	MISHCHENKO A, CHATTERJEE S, JIANG R, et al. FRAIGs: A unifying representation for logic synthesis and verification[R]. ERL Technical Report, 2005.
[39]	MISHCHENKO A, CHATTERJEE S, BRAYTON R, et al. Improvements to combinational equivalence checking[C]. The 2006 IEEE/ACM International Conference on Computer-Aided Design, San Jose, USA, 2006: 836–843. doi: 10.1145/1233501.1233679.
[40]	MISHCHENKO A, ZHANG J S, SINHA S, et al. Using simulation and satisfiability to compute flexibilities in Boolean networks[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2006, 25(5): 743–755. doi: 10.1109/TCAD.2005.860955.
[41]	LEE S Y, RIENER H, and DE MICHELI G. External don’t cares in logic synthesis[M]. DRECHSLE R and HUHN S. Advanced Boolean Techniques: Selected Papers from the 15th International Workshop on Boolean Problems. Cham: Springer, 2023: 33–47. doi: 10.1007/978-3-031-28916-3_3.
[42]	LIU Zequn and CHENG Daizhan. Canonical form of Boolean networks[C]. 2019 Chinese Control Conference, Guangzhou, China, 2019: 1801–1806. doi: 10.23919/ChiCC.2019.8865729.
[43]	FENG June, ZHAO Rong, and CUI Yanjun. Simplification of logical functions with application to circuits[J]. Electronic Research Archive, 2022, 30(9): 3320–3336. doi: 10.3934/era.2022168.
[44]	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.
[45]	HAASWIJK W, SOEKEN M, AMARÙ L, et al. A novel basis for logic rewriting[C]. The 22nd Asia and South Pacific Design Automation Conference, Chiba, Japan, 2017: 151–156. doi: 10.1109/ASPDAC.2017.7858312.
[46]	PAN Hongyang and CHU Zhufei. Exact synthesis based on semi-tensor product circuit solver[C]. 2023 Design, Automation & Test in Europe Conference & Exhibition, Antwerp, Belgium, 2023: 1–6. doi: 10.23919/DATE56975.2023.10137287.
[47]	MISHCHENKO A, CHATTERJEE S, and BRAYTON R. Improvements to technology mapping for LUT-based FPGAs[C]. 2006 ACM/SIGDA 14th International Symposium on Field Programmable Gate Arrays, Monterey, USA, 2006: 41–49. doi: 10.1145/1117201.1117208.
[48]	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, Florence, Italy, 2019: 1649–1654. doi: 10.23919/DATE.2019.8715185.
[49]	RIENER H, LEE S Y, MISHCHENKO A, et al. Boolean rewriting strikes back: Reconvergence-driven windowing meets resynthesis[C]. The 27th Asia and South Pacific Design Automation Conference, Taipei, China, 2022: 395–402. doi: 10.1109/ASP-DAC52403.2022.9712526.
[50]	PAN Hongyang, XIA Yinshui, WANG Lunyao, et al. Semi-tensor product based exact synthesis for logic rewriting[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2023. doi: 10.1109/TCAD.2023.3337279.
[51]	MISHCHENKO A, CHATTERJEE S, and BRAYTON R. DAG-aware AIG rewriting a fresh look at combinational logic synthesis[C]. The 43rd Annual Design Automation Conference, San Francisco, USA, 2006: 532–535. doi: 10.1145/1146909.1147048.
[52]	MISHCHENKO A and BRAYTON R. Integrating an AIG package, simulator, and SAT solver[C]. The International Workshop on Logic and Synthesis, Linz, Austria, 2018: 11–16.
[53]	AMARÚ L, MARRANGHELLO F, TESTA E, et al. SAT-sweeping enhanced for logic synthesis[C]. The 57th ACM/IEEE Design Automation Conference, San Francisco, USA, 2020: 1–6. doi: 10.1109/DAC18072.2020.9218691.
[54]	ZHU Qi, KITCHEN N, KUEHLMANN A, et al. SAT sweeping with local observability don't-cares[C]. The 43rd ACM/IEEE Design Automation Conference, San Francisco, USA, 2006: 229–234. doi: 10.1109/DAC.2006.229206.
[55]	PAN Hongyang and CHU Zhufei. Semi-tensor product based circuit simulation for SAT sweeping[C]. The International Workshop on Logic and Synthesis, Lausanne, Switzerland, 2023.
[56]	KRICHEN M. A survey on formal verification and validation techniques for internet of things[J]. Applied Sciences, 2023, 13(14): 8122. doi: 10.3390/app13148122.
[57]	卢山. 基于半张量积的模型检验方法的研究与实现[D]. [硕士论文], 电子科技大学, 2014. LU Shan. Research and implementation of model checking method based on semi-tensor product[D]. [Master dissertation], University of Electronic Science and Technology of China, 2014.
[58]	ZHAN Jinyu, LU Shan, and YANG Guowu. Improved calculation scheme of structure matrix of Boolean network using semi-tensor product[C]. The 3rd International Conference on Information Computing and Applications, Chengde, China, 2012: 242–248. doi: 10.1007/978-3-642-34038-3_33.
[59]	ZHAN Jinyu, LU Shan, and YANG Guowu. Analysis of boolean networks using an optimized algorithm of structure matrix based on semi-tensor product[J]. Journal of Computers, 2013, 8(6): 1441–1448. doi: 10.4304/jcp.8.6.1441-1448.
[60]	NETO W L, AUSTIN M, TEMPLE S, et al. LSOracle: A logic synthesis framework driven by artificial intelligence: Invited paper[C]. 2019 IEEE/ACM International Conference on Computer-Aided Design, Westminster, USA, 2019: 1–6. doi: 10.1109/ICCAD45719.2019.8942145.
[61]	HAASWIJK W, COLLINS E, SEGUIN B, et al. Deep learning for logic optimization algorithms[C]. 2018 IEEE International Symposium on Circuits and Systems, Florence, Italy, 2018: 1–4. doi: 10.1109/ISCAS.2018.8351885.
[62]	YANG Chenghao, XIA Yinshui, CHU Zhufei, et al. Logic synthesis optimization sequence tuning using RL-based LSTM and graph isomorphism network[J]. IEEE Transactions on Circuits and Systems II:Express Briefs, 2022, 69(8): 3600–3604. doi: 10.1109/TCSII.2022.3168344.
[63]	WU Nan, LI Yingjie, HAO Cong, et al. Gamora: Graph learning based symbolic reasoning for large-scale boolean networks[C]. The 60th ACM/IEEE Design Automation Conference, San Francisco, USA, 2023: 1–6,doi: 10.1109/DAC56929.2023.10247828.
[64]	程代展, 齐洪胜, 刘挺, 等. 从矩阵半张量积到逻辑控制系统: 献给陈翰馥教授80华诞[J]. 中国科学:数学, 2016, 46(10): 1401–1424. doi: 10.1360/N012015-00381. CHENG Daizhan, QI Hongsheng, LIU Ting, et al. From semi-tensor product of matrices to logical control systems[J]. Scientia Sinica:Mathematica, 2016, 46(10): 1401–1424. doi: 10.1360/N012015-00381.
[65]	FAN Longfei and WU Chang. FPGA technology mapping with adaptive gate decomposition[C]. The 2023 ACM/SIGDA International Symposium on Field Programmable Gate Arrays, Monterey, USA, 2023: 135–140. doi: 10.1145/3543622.3573048.
[66]	KUBICA M, OPARA A, and KANIA D. Technology mapping for LUT-Based FPGA[M]. Cham: Springer, 2021: 119–132. doi: 10.1007/978-3-030-60488-2.
[67]	CHENG Daizhan and XU Xiangru. Bi-decomposition of multi-valued logical functions and its applications[J]. Automatica, 2013, 49(7): 1979–1985. doi: 10.1016/j.automatica.2013.03.013.
[68]	LIU Fengqiu, YAN Ming, MAO Yuxin, et al. Application of semi-tensor product-based Bi-decomposition to FPGA mapping[C]. The 41st Chinese Control Conference, Hefei, China, 2022: 5945–5949. doi: 10.23919/CCC55666.2022.9901693.