Research

Boolean SAT Methods for Physical Design Problems

Group Members: R. Glenn Wood, Hui Xu

Collaborators: Gi-Joon Nam, IBM Austin Research Labs; Karem Sakallah, U. Michigan

Boolean Satisfiability (or “SAT”) is the problem of deciding if a large, complex Boolean equation is satisfiable, i.e., if there is any assignment of 0s and 1s to its component variables that renders the overall equation identically “1”. If not, the problem is unsatisfiable. Advances in representations (BDDs) and solvers (SAT) for the problem make it possible to consider formulating some non-Boolean problems into this Boolean form. Our work in this area mainly targets routing problems from the world of FPGAs. Our early paper in ISFPGA97 was the first to concretely pose the problem of discrete FPGA routing as a SAT problem. Subsequent advances in both the formulation and the sophistication on SAT solvers made it possible to target some extremely complex geometric problems, and even some novel general-purpose problems such as deciding which subset of constraints one might need to abandon to reach a partial (“sub-satistfiable”) solution to the problem.

Key Papers/Talks

  • R. Glenn Wood and Rob A. Rutenbar, “FPGA routing and routability estimation via Boolean satisfiability,” Proc. ACM International Symposium on FPGAs, Feb. 1997. pdf
  • R. Glenn Wood and Rob A. Rutenbar, “FPGA routing and routability estimation via Boolean satisfiability,” IEEE Trans on VLSI Systems, Vol. 6, No. 2, June 1998. pdf
  • G.-J. Nam, K. Sakallah and R. Rutenbar, “Satisfiability-based FPGA routing,” Proc. International Conference on VLSI Design, Jan. 1999, Goa, India.
  • G.-J. Nam, K. Sakallah and R. Rutenbar, “Satisfiability-based layout revisited: detailed routing of complex FPGAs via search-based boolean SAT,” Proc. ACM International Symposium on Field Programmable Gate Arrays, Feb. 1999.pdf
  • G.-J. Nam, K. Sakallah and R. Rutenbar, “A boolean satisfiability-based incremental rerouting approach with application to FPGAs,” Proc. Design Automation and Test in Europe (DATE01), March 2001. pdf
  • G.-J. Nam, F. Aloul, K. Sakallah and R. Rutenbar , “A comparative study of two boolean formulations on FPGA detailed routing constraints,” Proc. ACM International Symposium on Physical Design (ISPD01), April, 2001. pdf
  • Hui Xu, Rob A. Rutenbar, Karem Sakallah, “sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing,” Proc. ACM International Symposium on Physical Design (ISPD02), April 2002. pdf
  • G.-J. Nam, K. Sakallah and R. Rutenbar, “A new FPGA detailed routing approach via search-based boolean satisfiability,” IEEE Transactions on CAD, vol.21, no.6, June 2002. pdf
  • G.-J. Nam, K. Sakallah and R. Rutenbar , “Hybrid routing for FPGAs by integrating boolean safisfiability with geometric search,” International Conference on Field Programmable Logic and Applications, Sep. 2002, La Motte, France.
  • Hui Xu, Rob A. Rutenbar, Karem Sakallah, “sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing,” IEEE Trans CAD, Vol 22, No 6, June 2003. pdf
  • G.-J. Nam, F. Aloul, K. Sakallah and R. Rutenbar , “A comparative study of two boolean formulations on FPGA detailed routing constraints,” IEEE Transactions on Computers, vol. 53, no.6, June 2004. pdf

Copyright © 2015 Rob A. Rutenbar. All Rights Reserved. Site designed by Academic Web Pages