基于约束的FPGA详细布线

摘要

现场可编程逻辑门阵列(FPGA，Field Programmable Gate Array)，是一个含有可编辑元件的半导体设备，可供使用者现场程式化逻辑门阵列元件。目前以硬件描述语言(Verilog或VHDL)所完成的电路设计，可以经过综合与布局布线，快速烧录至FPGA上进行测试。
　　 本文主要研究基于约束的FPGA详细布线问题，即通过将详细布线问题转化为约束表达式并求解以得到可行的详细布线结果。本文中将分别使用SAT，SMT，CSP三种技术作为求解引擎来解决这个问题。
　　 SAT(Boolean satisfiability problem)求解器用来解决对于给定的布尔方程式，是否存在一组变量赋值，使间题可满足。因此，结合所要实现的口标，需要设计实现一个分析转换程序，将详细布线问题转换为一组可满足性问题的布尔方程式，从而可利用SAT问题求解器进行求解。在转换过程中，尤其需要注意的是原问题与目标问题的等价，即转换后的布尔方程能精确描述布线过程中的各类约束，从而得到可用的详细布线结果。
　　 SMT(Satisfiability Modulo Theories)工具与SAT工具一样都是用来解决命题逻辑可满足性问题。但不同的是，SAT仅仅能解决命题逻辑可满足问题，而SMT可以解决更为广泛的逻辑判定问题，这些问题可以包含整数变量，实数变量等。CSP(constraint satisfaction problem)在指定域中求出满足所有给定约束的子集，这些结果集满足所有的约束。本文中同样构建了FPGA详细布线问题向SMT和CSP问题精确的分析转换程序。要求与SAT问题类似，这里不再复述。
　　 针对上述三类问题的分析转换程序实现后，利用MCNC标准电路进行测试，分别统计转换程序与求解程序的时间与卒间消耗。分析得到的实验结果，并在实验结果的基础上提出改进方法，以期能找到一种在时间和空间上双优的FPGA详细布线算法。