伪布尔可满足性算法及其在fpga布线中的研究应用的论文

《伪布尔可满足性算法及其在fpga布线中的研究应用的论文》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、——j■一嘲。摘要’’VV现场可编程门阵列(FPGA)主要包括可配置逻辑模块和布线模块，它支持可编程重复配置，具有灵活、风险低、开发周期短等优势，在通信、工业控制、汽车电子、数据处理、消费电子等领域得到了广泛应用。随着FPGA内部可配置资源容量的增加，对应的计算机辅助设计(CAD)工具也需要升级和优化。随着设计复杂程度的提高，将一个设计配置到FPGA上往往需要CAD工具计算很长时间方可满足各种参数要求。而布线阶段通常需要消耗整个CAD流程近30％的时间，因此，高效的布线算法对缩短整个FPGA开发的时间至关重要。目前已开发多种布线算法并获得应用

2、，其中布尔可满足性(SAT)布线算法及几何查找布线算法是当前最为流行的两种。两者各有优缺点。基于几何查找的布线算法由基本迷宫(Maze)算法演化而来，它虽然可经过优化来提高布线速度，但由于一次只能布一根线，其可布通性较难确定，通常依靠设定运行时间的上限来实现算法终止。另外，其它由迷宫算法优化演化而来的各种几何查找算法也均存在依赖布线顺序的缺点。相比之下，基于SAT的算法由于可同时给所有线网布线，因此能从理论上证明可布通性。但是，这种算法需要大量的变量和约束条件，所以可扩展性并不好。最近，一种基于伪布尔可满足性(PBS)的布线算法成为FPGA布

3、线算法的研究热点。和一般基于SAT的算法类似，PBS算法可同时给所有线网进行布线，因此也能准确判断可布通性。和SAT算法不同的是，它将约束条件用精简的表达式表示，需要的布线变量和公式大大减少，因此显著降低了内存需求，提高了扩展性。但是，伪布尔可满足性算法在布线过程中所需的转换成本过大，不适用于大型布线基准。本文探索一种能有效解决以上问题的新型算法，具体研究工作和结果如下：(1)在全面调查FPGA结构最新研究动态的基础上，给出了一种FPGA布线结构模型，即基于S删的对称阵列(岛状)FPGA结构，仅需3个适合的参数即能表示布线结构。详细研究了布尔

4、可满足性算法、伪布尔可满足性算法和两种几何查找布线算法，即一种基于协商性能驱动的布线算法PatllFinder和一种协商A幸布线算法Frontier。选取全局布线实例和MaX．SAT布线基准的大规模基准电路，对Frontier、SAT和PBS进行了分析比较。结果表明，利用伪布尔约束编码比用纯粹的合取范式(CNF)显示出更好的紧密性、更短的运行时间，且编码更简洁紧凑。针对伪布尔可满足性问题扩展开发的解法器PBS，与以前所报道的两种方法相比较——早期的几何查找算法和现在用于纯CNF约束的解法器Cham从而验证了伪布尔可满足性所需存储空间更小，并能

5、有效加速求解的特性。(2)近年来0．1整数线性规划(IntegerLineafProgramming，ILP)的发展进一步扩展了优化线性目标函数，这通常是通过解决一系列的SAT或者ILP决策问题来实现的。但是目标函数可能会使采用对称的约束变得复杂化，即使目标函数的约束不可满足，并且与目标函数不相关。本文在对称破缺技术的基础上，开发了一种自适应流程，结合静态对称破缺技术和动态对称破缺技术，可以分析一个给定的布尔优化问题，并能挑选最摘要合适的对称破缺技术。实验结果证明，当这种技术用于布线时，比纯粹的静态对称破缺或动态对称破缺加速了问题的解决。(3

6、)为了改善伪布尔可满足性算法在布线过程中增加转换成本的负面影响，提出了一种用于FPGA的新的布线算法，综合了伪布尔可满足性算法与几何布线算法的优点。在布线过程中，先选用Frontier或PathFinder这类几何布线算法对FPGA进行布线，如果不能成功再采用伪布尔可满足性算法。并在布线流程中增加了静态对称破缺技术对伪布尔约束进行预处理，侦测并破缺其中的对称，减少搜索路径，从而减少成本。实验结果表明，这种混合布线方法可以显著减少运行时间，加速求解过程。(4)研究了用子集可满足性(sub．SAT)算法求解FPGA详细布线的问题。在布线资源固定的

7、FPGA布线环境中，布尔公式可以证明所给电路的不可布通性，优于典型的one-net-at．a．time方法。子集可满足性方法把一个有Ⅳ个约束的“严格的”SAT问题转换成一个新的“松弛的”SAT问题，仅当在原始问题中变量的不可满足个数不超过阈值七(七“Ⅳ)时，这一问题是可满足的。它改进了布尔可满足性，但是却产生了很多额外的变量和子句。针对这一问题，提出了两种改进方法。第一，用伪布尔可满足性(PBS)来消除子集可满足性公式带来的缺点。第二，针对子集可满足性算法在求解同时增加额外的变量和字句，而使得对称数量按指数级增长的问题，选用增加静态对称破缺的

8、方法对CNF进行预处理，侦测并破缺其中的对称，从而达到减少搜索路径的目的。用简化图自同构的方法来侦测所有对称性，在增加合适的对称破缺判定(SBPs)后，限制搜索在空