一种加速FPGA布线的不可满足子式求解算法

doi:10.12263/DZXB.20200670

电子学报 ›› 2021, Vol. 49 ›› Issue (6): 1210-1216.DOI: 10.12263/DZXB.20200670

一种加速FPGA布线的不可满足子式求解算法

张建民, 黎铁军, 马柯帆, 肖立权

国防科学技术大学计算机学院, 湖南长沙 410073

收稿日期:2020-07-08 修回日期:2020-10-26 出版日期:2021-06-25 发布日期:2022-06-25
作者简介:张建民 男,1979年生于山西晋中.现为国防科技大学计算机学院副研究员.主要研究方向为可满足求解和VLSI形式化验证.E-mail:jmzhang@nudt.edu.cn;黎铁军 男,1977年生于湖北十堰.现为国防科技大学计算机学院研究员.主要研究方向为VLSI功能验证和微处理器体系结构.E-mail:tjli@nudt.edu.cn;马柯帆 男,1985年生于湖南永州.现为国防科技大学计算机学院助理研究员.主要研究方向为可满足求解和FPGA加速.E-mail:makefan14@nudt.edu.cn;肖立权 男,1969年生于湖北孝感.现为国防科技大学计算机学院研究员,博士生导师.主要研究方向为高性能计算机体系结构.E-mail:lqxiao2015@163.com
基金资助:
国家自然科学基金（No.62072464，No.U19A2062）；并行与分布处理国家级重点实验室开放基金（No.WDZC20205500116）

An Unsatisfiable Subformula Computing Algorithm to Accelerate FPGA Routing

ZHANG Jian-min, LI Tie-jun, MA Ke-fan, XIAO Li-quan

School of Computer, National University of Defense Technology, Changsha, Hunan 410073, China

Received:2020-07-08 Revised:2020-10-26 Online:2021-06-25 Published:2022-06-25

摘要/Abstract

摘要： 随着VLSI（Very Large Scale Integrated）芯片设计的规模越来越大，功能越来越复杂，在FPGA（Field Programmable Gate Array）上实现或进行原型验证时，往往会出现布线拥塞或无法布通的情况.而不可满足子式能够迅速诊断FPGA无法布通的原因，并且精确定位关键线网.针对如何加速FPGA详细布线过程，提出了一种基于消解否证的启发式局部搜索算法，能够快速从布尔公式中提取不可满足子式.基于典型的FPGA布线测试集，与两种求解最小不可满足子式效率最高的算法进行了比较，结果表明局部搜索算法在运行效率方面显著优于分支限界算法与贪心遗传算法，而局部搜索算法也能得到最小不可满足子式；并且深入分析了不可满足子式在FPGA详细布线中的作用，能够加速芯片的设计与验证过程.

关键词: FPGA布线, 布线约束, 布尔可满足性, 不可满足子式, 局部搜索, 消解否证

Abstract: With the growing scale and complexity of VLSI(Very Large Scale Integrated) chip designs,the FPGA(Field Programmable Gate Array) detailed routing process generally meets the congestion or unroutable problems during the FPGA implementation or prototype verification.The unsatisfiable subformulas can quickly diagnose the FPGA unroutable root cause,and accurately localize the critical nets.In order to accelerate the FPGA routing process,we have proposed a heuristic local search algorithm based on resolution refutation,to derive the unsatisfiable subformulas from the Boolean formulas.On the typical FPGA routing benchmarks,the local search algorithm has been compared to the two optimal minimum unsatisfiable subformula extraction algorithms.The experimental results show that the local search algorithm strongly outperforms the branch-bound algorithm and the greedy generic algorithm,and it also obtains the minimum unsatisfiable subformula.Furthermore,the unsatisfiable subformula plays an important role in FPGA routing,and it can improve the efficiency of design and verification of the VLSI chips.

Key words: FPGA routing, routing constraint, Boolean satisfiability, unsatisfiable subformula, local search, resolution refutation

中图分类号:

TP391

张建民, 黎铁军, 马柯帆, 肖立权. 一种加速FPGA布线的不可满足子式求解算法[J]. 电子学报, 2021, 49(6): 1210-1216.

ZHANG Jian-min, LI Tie-jun, MA Ke-fan, XIAO Li-quan. An Unsatisfiable Subformula Computing Algorithm to Accelerate FPGA Routing[J]. Acta Electronica Sinica, 2021, 49(6): 1210-1216.

参考文献

[1] Nam G J,Aloul F,Sakallah K,et al.A comparative study of two Boolean formulations of FPGA detailed routing constraints[A].Proceedings of the 2001 International Symposium on Physical Design[C].Sonoma County,CA,USA:ACM,2001.222-227.
[2] Liffiton M H,Mneimneh M N,Lynce I,et al.A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas[J].Constraints,2009,14(4):415-442.
[3] 张建民,沈胜宇,李思昆.最小布尔不可满足子式的求解算法[J].电子学报,2009,9(5):993-999. Zhang Jianmin,Shen Shengyu,Li Sikun.Algorithm for deriving minimum unsatisfiable subformulae[J].Acta Electronica Sinca,2009,9(5):993-999.(in Chinese)
[4] Oh Y,Mneimneh M N,Andraus Z S,et al.AMUSE:a minimally-unsatisfiable subformula extractor[A].Proceedings of the 41st Design Automation Conference[C].San Diego,CA,USA:ACM,2004.518-523.
[5] Li Xiaowei,Li Guanghui,Shao Ming.Formal verification techniques based on Boolean satisfiability problem[J].Journal of Computer Science and Technology,2005,20(1):38-47.
[6] Liffiton MH,Sakallah KA.Algorithms for computing minimal unsatisfiable subsets of constraints[J].Journal of Automated Reasoning,2008,40:1-30.
[7] 陈振宇,徐宝文,周从华.一种基于消解的变量极小不可满足子公式的提取方法[J].计算机研究与发展,2008,45(s1):43-47. Chen Zhenyu,Xu Baowen,Zhou Conghua.A resolution-based approach for extracting variable minimal unsatisfiable subformulas[J].Journal of Computer Research and Development,2008,45(s1):43-47.(in Chinese)
[8] 赵相福,欧阳丹彤.使用SAT求解器产生所有极小冲突部件集[J].电子学报,2009,37(4):804-810. Zhao Xiangfu,Ouyang Dantong.Deriving all minimal conflict sets using satisfiability algorithms[J].Acta Electronica Sinica,2009,37(4):804-810.(in Chinese)
[9] Nadel A.Boosting minimal unsatisfiable core extraction[A].Proceedings of the 10th International Conference on Formal Methods in Computer Aided Design[C].Lugano,Switzerland:IEEE,2010.221-229.
[10] Marques-Silva J,Lynce I.Onimproving MUS extraction algorithms[A].Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing[C].Ann Arbor,MI,USA:Springer,2011.159-173.
[11] Belov A,Lynce I,Marques-Silva J.Towards efficient MUS extraction[J].Journal AI Communications,2012,25(2):97-116.
[12] Nadel A,Ryvchin V,Strichman O.Efficient MUS extraction with resolution[A].Proceedings of the 13th International Conference Formal Methods in Computer Aided Design[C].Portland,OR,USA:IEEE,2013.197-200.
[13] Marques-Silva J,Previti A.On computing preferred MUSes and MCSes[A].Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing[C].Vienna,Austria:Springer,2014.58-74.
[14] Bacchus F,Katsirelos G.Using minimal correction sets to more efficiently compute minimal unsatisfiable sets[A].Proceedings of the 27th International Conference on Computer Aided Verification[C].San Francisco,CA,USA:Springer,2015.70-86.
[15] Bacchus F,Katsirelos G.Finding a collection of MUSes incrementally[A].Proceedings of the 13th International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems[C].Banff,AB,Canada:Springer,2016.35-44.
[16] Zhao W,Liffiton M H.Parallelizing partial MUS enumeration[A].Proceedings of IEEE 28th International Conference on Tools with Artificial Intelligence[C].San Jose,CA,USA:IEEE,2016.464-471.
[17] Gregoire E,Izza Y.Boosting MCSes enumeration[A].Proceedings of the 27th International Joint Conference on Artificial Intelligence[C].Stockholm,Sweden:ACM,2018.1309-1315.
[18] Narodytska N,Bjorner N,Marinescu M C,et al.Core-guided minimal correction set and core enumeration[A].Proceedings of the 27th International Joint Conference on Artificial Intelligence[C].Stockholm,Sweden:ACM,2018.1353-1361.
[19] Liu Shaofan,Luo Jie.FMUS2:An efficient algorithm to compute minimal unsatisfiable subsets[A].Proceedings of 2018 International Conference on Artificial Intelligence and Symbolic Computation[C].Suzhou,China:Springer,2018.104-118.
[20] Luo Jie,Liu Shaofan.Accelerating MUS enumeration by inconsistency graph partitioning[J].Science China Information Sciences,2019,62:212104.
[21] Mencia C,Kullmann O,Ignatiev A,Marques-Silva J.On computing the union of MUSes[A].Proceedings of 22nd International Conference on Theory and Applications of Satisfiability Testing[C].Lisbon,Portugal:Springer,2019.211-221.
[22] Jaroslav B,Kuldeep MS.Approximate counting of minimal unsatisfiable subsets[A].Proceedings of the 32nd International Conference on Computer Aided Verification[C].Los Angeles,CA,USA:Springer,2020.1-23.
[23] Jaroslav B,Cerna I.Rotation based MSS/MCS enumeration[A].Proceedings of the 23rd International Conference on Logic for Programming,Artificial Intelligence and Reasoning[C].Alicante,Spain:EasyChair,2020.120-137.
[24] Jaroslav B,Cerna I.MUST:minimal unsatisfiable subsets enumeration tool[A].Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[C].Dublin,Ireland:Springer,2020.135-152.
[25] Gallier J H.Logic for Computer Science:Foundations of Automatic Theorem Proving[M].New York:Harper & Row Publishers Inc,2003.

一种加速FPGA布线的不可满足子式求解算法

An Unsatisfiable Subformula Computing Algorithm to Accelerate FPGA Routing

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 12

编辑推荐

Metrics

[1]	王金艳, 胡春, 牛当当, 李先贤. 基于IAPS的扩展规则局部搜索算法[J]. 电子学报, 2020, 48(5): 899-905.
[2]	曹玉莲, 李文锋, 张煜. 基于拟熵自适应启动局部搜索策略的混合粒子群算法[J]. 电子学报, 2018, 46(1): 110-117.
[3]	王春, 田娜, 纪志成, 王艳. 求解模糊柔性作业车间调度的多目标进化算法[J]. 电子学报, 2017, 45(12): 2909-2916.
[4]	续欣莹, 张扩, 谢珺, 谢刚. 基于互信息下粒子群优化的属性约简算法[J]. 电子学报, 2017, 45(11): 2695-2704.
[5]	叶东毅, 陈昭炯. 最小属性约简问题的一个有效的组合人工蜂群算法[J]. 电子学报, 2015, 43(5): 1014-1020.
[6]	王令赛, 姜淑娟, 张艳梅, 于巧. 基于正交搜索的粒子群优化测试用例生成方法[J]. 电子学报, 2014, 42(12): 2345-2351.
[7]	尹浩, 张长胜, 张斌, 孙若男, 刘婷婷. 一种求解SLA等级感知服务组合问题的多目标离散粒子群优化算法[J]. 电子学报, 2014, 42(10): 1983-1990.
[8]	莫宏伟, 徐立芳. 基于Memetic算法的电路演化设计研究[J]. 电子学报, 2013, 41(5): 1036-1040.
[9]	张雪霞;陈维荣;戴朝华. 带局部搜索的动态多群体自适应差分进化算法及函数优化[J]. 电子学报, 2010, 38(8): 1825-1830.
[10]	张建民;沈胜宇;李思昆. 最小布尔不可满足子式的求解算法[J]. 电子学报, 2009, 37(5): 993-999.
[11]	刘红;白栋;丁炜;曾志民. 多目标的Internet路由优化控制算法[J]. 电子学报, 2004, 32(2): 306-309.
[12]	孙元凯;刘民;吴澄. 变邻域结构Tabu搜索算法及其在JobShop调度问题上的应用[J]. 电子学报, 2001, 29(5): 622-625.