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

An Unsatisfiable Subformula Computing Algorithm to Accelerate FPGA Routing

随着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.