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

doi:10.12263/DZXB.20200670

PDF(1052 KB)

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

学术论文

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

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

作者信息 +

An Unsatisfiable Subformula Computing Algorithm to Accelerate FPGA Routing

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

Author information +

文章历史 +

摘要

随着VLSI（Very Large Scale Integrated）芯片设计的规模越来越大，功能越来越复杂，在FPGA（Field Programmable Gate Array）上实现或进行原型验证时，往往会出现布线拥塞或无法布通的情况.而不可满足子式能够迅速诊断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.

导出引用

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

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. https://doi.org/10.12263/DZXB.20200670

中图分类号： TP391

参考文献

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