Boolean Satisfiability-Based Routing and Its Application to Xilinx UltraScale Clock Network
Boolean Satisfiability-Based Routing and Its Application to Xilinx UltraScale Clock Network
复制标题
基于布尔可满足性的路由及其在 Xilinx UltraScale 时钟网络中的应用
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
A. Kaviani
中科院分区：
文献类型：
--
作者：
H. Fraisse;A. Joshi;D. Gaitonde;A. Kaviani
布尔可满足性（SAT）为基础的路由提供了一个独特的优势，传统的路由算法，提供了一个详尽的方法来找到一个解决方案。尽管有这个优势，但由于可扩展性问题，商业FPGA CAD工具很少使用基于SAT的路由器。在本文中，我们重新审视基于SAT的路由，并提出了两个SAT配方独立的路由架构。然后，我们证明，SAT为基础的路由使用任何配方显着优于传统的路由算法在运行时间和鲁棒性的时钟路由的Xilinx UltraScale设备。最后，我们的实验表明，提出的SAT公式之一导致路由18倍更快，并产生公式20倍更紧凑比其他。该框架已在Vivado中实现，目前正在生产中使用。
Boolean Satisfiability (SAT)-based routing offers a unique advantage over conventional routing algorithms by providing an exhaustive approach to find a solution. Despite that advantage, commercial FPGA CAD tools rarely use SAT-based routers due to scalability issues. In this paper, we revisit SAT-based routing and propose two SAT formulations independent of routing architecture. We then demonstrate that SAT-based routing using either formulation dramatically outperforms conventional routing algorithms in both runtime and robustness for the clock routing of Xilinx UltraScale devices. Finally, we experimentally show that one of the proposed SAT formulations leads to a routing 18x faster and produces formulas 20x more compact than the other. This framework has been implemented into Vivado and is now currently used in production.