Research Progress in Logic Synthesis Based on Semi-Tensor Product

CHU Zhufei; MA Chengyu; YAN Ming; PAN Jiaxiang; PAN Hongyang; WANG Lunyao; XIA Yinshui

doi:10.11999/JEIT231457

Article Contents

Article Navigation > Journal of Electronics & Information Technology > 2022 >

CHU Zhufei, MA Chengyu, YAN Ming, PAN Jiaxiang, PAN Hongyang, WANG Lunyao, XIA Yinshui. Research Progress in Logic Synthesis Based on Semi-Tensor Product[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT231457

Citation:

CHU Zhufei, MA Chengyu, YAN Ming, PAN Jiaxiang, PAN Hongyang, WANG Lunyao, XIA Yinshui. Research Progress in Logic Synthesis Based on Semi-Tensor Product[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT231457

Citation:

PDF( 2086 KB)

Research Progress in Logic Synthesis Based on Semi-Tensor Product

doi: 10.11999/JEIT231457

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)

Received Date: 2024-01-09
Rev Recd Date: 2024-03-15

Available Online: 2024-03-21

Abstract

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)

FullText(HTML)

References(68)

References

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