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

• 学术论文 • 上一篇    下一篇

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

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

  1. 国防科学技术大学计算机学院, 湖南长沙 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   

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

摘要: 随着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

中图分类号: