Issue No. 06 - June (2004 vol. 53)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2004.1
Karem A. Sakallah , IEEE
Rob A. Rutenbar , IEEE
Gi-Joon Nam , IEEE
<p><b>Abstract</b>—This paper presents empirical analyses of two Boolean Satisfiability (SAT) formulations of FPGA (Field Programmable Gate Array) detailed routing constraints. Boolean SAT-based routing transforms a routing problem into a Boolean SAT instance by rendering geometric routing constraints as an atomic Boolean function. The generated Boolean function is satisfiable if and only if the corresponding routing is possible. Two different Boolean SAT-based routing models are analyzed: the <it>track-based</it> and the <it>route-based</it> routing constraint model. The track-based routing model transforms a routing task into a net-to-track assignment problem, whereas the route-based routing model reduces it into a routability-checking problem with explicitly enumerated set of detailed routes for nets. In both models, routing constraints are represented as CNF Boolean Satisfiability clauses. Through comparative experiments, we demonstrate that the route-based formulation yields an easier-to-evaluate and more scalable routability Boolean function than the track-based method. This is empirical evidence that a smart/efficient Boolean formulation can achieve significant performance improvement in real-world applications.</p>
Boolean Satisfiability, FPGAs, routing, physical design.
Karem A. Sakallah, Rob A. Rutenbar, Gi-Joon Nam, Fadi Aloul, "A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints", IEEE Transactions on Computers, vol. 53, no. , pp. 688-696, June 2004, doi:10.1109/TC.2004.1