| 基于改进型SAT求解器算法的组合电路等价性检查研究 |
| |
| 引用本文： | 屈展,李康,刘鸿瑾,张绍林,李宾,周游,史江义,祁仲冬.基于改进型SAT求解器算法的组合电路等价性检查研究[J].微电子学,2023,53(1):109-114. |
| |
| 作者姓名： | 屈展 李康 刘鸿瑾 张绍林 李宾 周游 史江义 祁仲冬 |
| |
| 作者单位： | 西安电子科技大学 微电子学院, 西安 710071;北京轩宇空间科技有限公司, 北京 100190 |
| |
| 基金项目： | 西安电子科技大学校企合作项目(HX07202012009) |
| |
| 摘 要： | 随着工艺节点的缩小，集成电路规模的增加，集成电路设计过程中逻辑等价性检查在确保设计功能正确性方面起着重要作用。文章研究了组合电路逻辑等价性检查技术，针对该领域常用的DPLL和CDCL算法存在的问题，提出了一种基于蒙特卡洛树搜索的改进算法。通过对ISCAS85测试集的一个子集的实验，证实该算法对CDCL算法有一定的改进，应用于组合电路等价性检查的平均运行时间减少了20%。
|
| 关 键 词： | 等价性检查 组合电路 可满足性问题 EDA |
| 收稿时间： | 2021/12/19 0:00:00 |
Research on Equivalence Checking of Combinational Circuits Based onImproved SAT Solver Algorithm |
| |
| QU Zhan,LI Kang,LIU Hongjin,ZHANG Shaolin,LI Bin,ZHOU You,SHI Jiangyi,QI Zhongdong.Research on Equivalence Checking of Combinational Circuits Based onImproved SAT Solver Algorithm[J].Microelectronics,2023,53(1):109-114. |
| |
| Authors: | QU Zhan LI Kang LIU Hongjin ZHANG Shaolin LI Bin ZHOU You SHI Jiangyi QI Zhongdong |
| |
| Abstract: | With the reduction of process nodes and the increase of complexity of integrated circuit scale, the logic equivalence check plays an important role in ensuring the correctness of design functions in the process of integrated circuit design. The logic equivalence checking technology of combinational circuits was studied in this paper. Aiming at the problems of DPLL and CDCL algorithms commonly used in this field, an improved algorithm based on Monte Carlo tree search was proposed to solve the satisfiable problem. Through the experiment on a subset of ISCAS85 test set, it is proved that the algorithm has a certain improvement on CDCL algorithm, and the average running time applied to combinational circuit equivalence check is reduced by about 20%. |
| |
| Keywords: | equivalence checking combinational circuit satisfiability problem (SAT) EDA |
|
| 点击此处可从《微电子学》浏览原始摘要信息 |
| 点击此处可从《微电子学》下载免费的PDF全文 |
|
