This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints
June 2004 (vol. 53 no. 6)
pp. 688-696
ASCII Text
x 
 
Gi-Joon Nam, Fadi Aloul, Karem A. Sakallah, Rob A. Rutenbar, "A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints," IEEE Transactions on Computers, vol. 53, no. 6, pp. 688-696, June, 2004.
 
 
BibTex
x
 
@article{ 10.1109/TC.2004.1,
author = {Gi-Joon Nam and Fadi Aloul and Karem A. Sakallah and Rob A. Rutenbar},
title = {A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints},
journal ={IEEE Transactions on Computers},
volume = {53},
number = {6},
issn = {0018-9340},
year = {2004},
pages = {688-696},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2004.1},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints
IS - 6
SN - 0018-9340
SP688
EP696
EPD - 688-696
A1 - Gi-Joon Nam,
A1 - Fadi Aloul,
A1 - Karem A. Sakallah,
A1 - Rob A. Rutenbar,
PY - 2004
KW - Boolean Satisfiability
KW - FPGAs
KW - routing
KW - physical design.
VL - 53
JA - IEEE Transactions on Computers
ER -
 

Abstract—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 track-based and the route-based 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.

[1] M.J. Alexander, J.P. Cohoon, J.L. Ganley, and G. Robins, Performance-Oriented Placement and Routing for Field-Programmable Gate Arrays Proc. European Design Automation Conf., 1995.
[2] M.J. Alexander and G. Robins, New Performance-Driven FPGA Routing Algorithms IEEE Trans. Computer-Aided Design, vol. 15, no. 12, pp. 1505-1517, Dec. 1996.
[3] R. Bayardo Jr. and R. Schrag, Using CSP Look-Back Techniques to Solve Real World SAT Instances Proc. 14th Nat'l Conf. Artificial Intelligence, pp. 203-208, 1997.
[4] V. Betz and J. Rose, VPR: A New Packing, Placement and Routing Tool for FPGA Research Proc. Seventh Ann. Workshop Field Programmable Logic and Applications, pp. 213-222, 1997.
[5] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs Proc. Tools and Algorithms for the Construction and Analysis of Systems, 1999.
[6] S. Brown, R. Francis, J. Rose, and Z. Vranesic, Field Programmable Gate Arrays. Boston: Kluwer Academic, 1992.
[7] M. Davis and H. Putnam, A Computing Procedure for Quantification Theory J. ACM, vol. 7, pp. 201-215, 1960.
[8] M. Davis, G. Longeman, and D. Loveland, A Machine Program for Theorem Proving Comm. ACM, vol. 5, no. 7, 1962.
[9] S. Devadas, "Optimal Layout via Boolean Satisfiability," Proc. Int'l Conf. Computer Aided Design (ICCAD), IEEE CS Press, Los Alamitos, Calif., 1989, pp. 294-297.
[10] M. Garey and D. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, 1979.
[11] E. Goldberg and Y. Novikov, BerkMin: A Fast and Robust SAT-Solver Proc. Design, Automation and Test in Europe Conf., pp. 142-149, 2002.
[12] T.Y.K. Kam and R.K. Brayton, Multi-Valued Decision Diagrams Technical Report UCB/ERL M90/125, Univ. of California at Berkeley, 1990.
[13] W. Kunz and D. Stoffel, Reasoning in Boolean Networks. Kluwer Academic, 1997.
[14] T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," IEEE Trans. Computer-Aided Design, pp. 6-22, Jan. 1992.
[15] Y.-S. Lee and A. Wu, A Performance and Routability Driven Router for FPGAs Considering Path Delays Proc. Design Automation Conf., pp. 557-561, 1995.
[16] G. Lemieux and S. Brown, A Detailed Router for Allocating Wire Segments in FPGAs Proc. ACM Physical Design Workshop, Apr. 1993.
[17] C.-M. Li, Integrating Equivalency Reasoning into Davis-Putnam Procedure Proc. Nat'l Conf. Artificial Intelligence, 2000.
[18] L.M. Silva and K.A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.
[19] L.E. McMurchie and C. Ebeling, PathFinder: A Negotiation-Based Path-Driven Router for FPGAs Proc. ACM/IEEE Int'l Symp. Field Programmable Gate Arrays, Feb. 1995.
[20] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver Proc. 38th Design Automation Conf., pp. 530-535, 2001.
[21] G.-J. Nam, K.A. Sakallah, and R.A. Rutenbar, A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability IEEE Trans. Computer-Aided Design, vol. 21, no. 6, June 2002.
[22] G.-J. Nam, F. Aloul, K. Sakallah, and R. Rutenbar, A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints Proc. Int'l Symp. Physical Design, 2001.
[23] J. Rose, W. Snelgrove, and Z. Vranesic, ALTOR: An Automatic Standard Cell Layout Program Proc. Canadian Conf. Very Large Scale Integration, pp. 169-173, Nov. 1985.
[24] B. Selman, H. Kautz, and B. Cohen, Local Search Strategies for Satisfiability Testing DIMACS Series in Discrete Math. and Theoretical Computer Science, vol. 26, pp. 521-532, 1996.
[25] N. Sherwani, Algorithms for VLSI Physical Design Automation. Boston: Kluwer Academic, 2000.
[26] K. Sulimma and W. Kunz, An Exact Algorithm for Solving Difficult Detailed Routing Problems Proc. ACM/IEEE Int'l Symp. Physical Design, Apr. 2001.
[27] T. Szymanski, Dogleg Channel Routing Is NP-Complete IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 4, no. 1, 1985.
[28] S. Wilton, Architectures and Algorithms for Field-Programmable Gate Arrays with Embedded Memories PhD dissertation, Univ. of Toronto, 1997.
[29] Y.L. Wu and M. Marek-Sadowska, “Routing for Array Type FPGAs,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 16, no. 5, pp. 506-518, May 1997.
[30] M.V. Velev and R.E. Bryant, Superscalar Processor Verification Using Efficient Reductions from the Logic of Equality with Uninterpreted Functions to Propositional Logic, , Proc. Correct Hardware Design and Verification Methods, pp. 37-53, 1999.
[31] R. Zabih and D.A. Mcallester, A Rearrangement Search Strategy for Determining Propositional Satisfiability Proc. Nat'l Conf. Artificial Intelligence, pp. 155-160, 1988.
[32] H. Zhang, SATO: An Efficient Propositional Prover Proc. Int'l Conf. Automated Deduction, pp. 272-275, 1997.

Index Terms:
Boolean Satisfiability, FPGAs, routing, physical design.
Citation:
Gi-Joon Nam, Fadi Aloul, Karem A. Sakallah, Rob A. Rutenbar, "A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints," IEEE Transactions on Computers, vol. 53, no. 6, pp. 688-696, June 2004, doi:10.1109/TC.2004.1
Usage of this product signifies your acceptance of the Terms of Use.