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

An Unsatisfiable Subformula Computing Algorithm to Accelerate FPGA Routing

作　　者：张建民[1] 黎铁军[1] 马柯帆[1] 肖立权[1] ZHANG Jian-min;LI Tie-jun;MA Ke-fan;XIAO Li-quan(School of Computer,National University of Defense Technology,Changsha,Hunan 410073,China)

机构地区：[1]国防科学技术大学计算机学院,湖南长沙410073

出　　处：《电子学报》2021年第6期1210-1216,共7页Acta Electronica Sinica

基　　金：国家自然科学基金(No.62072464,No.U19A2062);并行与分布处理国家级重点实验室开放基金(No.WDZC20205500116)。

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

分 类 号：TP391[自动化与计算机技术—计算机应用技术]