Routing under constraints

Abstract

Routing is an essential stage in physical design, where already placed components are connected by wires. Routing must satisfy various manufacturing requirements, referred to as design rules. We formalize the problem of design-rule-aware routing and introduce a solver, called DRouter, for the resulting problem. Plain routing is often modeled as follows: given an undirected weighted graph and a set of m disjoint nets (each net being a set of vertices), a routing is a (minimal) forest of m disjoint trees, where each tree spans a net. DRouter's input comprises a plain routing instance and a bit-vector formula, whose variables include the edges of the graph as Boolean variables (along with other variables). DRouter looks for a satisfying assignment to F, such that the satisfied edges comprise a routing. DRouter implements an A*-based router inside a SAT solver. It overrides the solver's decision and restart strategies and enhances its learning with routing-aware algorithms. We demonstrate that, on a set of crafted routing instances, DRouter has substantially better capacity than either plain reduction to bit-vector reasoning or Monosat, a solver that is able to reason about SAT and graph predicates. We show that DRouter can route large clips from Intel designs while obeying up to millions of applications of the design rules - a task two industrial routers failed to accomplish.