Typically, most physical design problems can be cast as classical optimization problems with one or more objective functions that must be maximized or minimized subject to a set of constraints. Specifically, many physical design problems are instances of integer linear programs (ILPs). As is well known, however, ILPs seem to be impractical to solve layout problems exactly except for small-scale problems despite its modeling ability. Boolean functions can be used to model integer linear inequalities. In particular, a system of m linear inequalities in n integer variables can be transformed into a single Boolean equation by a suitable binary encoding of the integer variables. Even though the Boolean satisfiability (SAT) problem fueled major advances in various electronic design automation (EDA) areas during the last decade, especially in logic synthesis, simulation, testing, formal functional and timing verification, the physical design domain has not been actively attacked using Boolean SAT approach except a few works [1][5][6]. This is mainly because of the false myth that Boolean SAT instances in layout problems are always so huge that they cannot be solved with reasonable computational resources. However, thanks to the significant progress made in SAT realm [7] during the current decade, large-scaled problems unsolvable only a few years ago are now quite affordable and this opens a new possibility of applying a Boolean SAT-based approach even in physical layout domains.
The purpose of this thesis is to investigate an alternative formulation of various physical design problems (especially placement, global and detailed routing) via Boolean SAT formulations. SAT problems are intrinsically "exact" methods; we create a large but atomic Boolean function whose internal structure captures the geometrical optimization we seek and respects the constraints we must obey. Then any satisfying assignment of Boolean values to variables which renders the Boolean function identically "1" represents a legal layout solution. Moreover, by demonstrating that there is no such satisfying Boolean assignment, we can prove the non-existence of any corresponding geometrical layout solutions.
The efficiency of this approach in the physical layout domain primarily depends upon the possibility of capturing and representing all the relevant layout constraints in Boolean domain. This relates to the ability to encode the original layout problem variables and constraints using a reasonable number of Boolean variables and constraints. Encodings that require an exponential number of variables/constraints are clearly undesirable and can render such transformation unusable. We have preliminary experimental evidence suggesting an affirmative answer to this question.
In our preliminary research [2][3], we developed a Satisfiability-based
Detailed FPGA Router (SDR) using a search-based satisfiability solver GRASP
[4]. Field programmable gate array (FPGAs) provide a good starting point
for applying the Boolean SAT-based formulation to geometric layout problems
because their fixed routing resources and rigid structure make it particularly
easy to model the problem of detailed route assignment in the Boolean domain.
We successfully transformed the geometric FPGA detailed routing task into
a large but single Boolean function, and the search-based SAT solver is
employed to find a routing solution if there is any. This formulation has
the virtue that it considers all nets simultaneously and route them concurrently,
unlike the traditional one-net-at-a-time routing approach, and the absence
of a satisfying assignment implies that the layout is unroutable. A few
points worth mentioning through this preliminary experiment are:
• The routing results of Boolean SAT-based formulation are quite comparable
to results of other routers using traditional geometric approach in terms
of the quality of solutions as well as runtime.
• The Boolean SAT-based formulation is flexible enough to allow us
to adapt to different routing architectures easily through simple Boolean
function manipulation.
• The Boolean SAT-based formulation is able to determine the infeasibility
of layout by showing that there is no "satisfying" Boolean assignments
of values to variables.
We strongly believe that a fresh examination of a subset of layout problems
as instances of Boolean optimization can yield significant insights into
the structure of these problems and potentially produce solutions that
have been unattainable thus far. This is a highly nontraditional method
of attack for physical design tasks, but one that has considerable promise.