Component Based Synthesis Applied to Bitvector Circuits

We define “component-based synthesis” to be the problem of synthesis
of (straight-line) programs from appropriate composition of base components
from a specified library of software components. The functional
specification of the desired program and the library components is
provided in the form of logical formulas that relate the respective input and
output variables. This has applications in design of intricate
circuits or algorithms, superoptimization, and API mining. Furthermore,
automated synthesis provides the promise of correctness by construction,
generation of efficient systems, and improvement in developer’s productivity.

We solve the component-based synthesis problem using a constraint-based
approach that involves first generating a “synthesis constraint”,
and then solving the constraint. The synthesis constraint is a first-order
logic formula whose size is quadratic in the number of components,
but has quantifier alternation. We present a novel algorithm for
solving such constraints. Our algorithm is based on counterexample
guided iterative synthesis paradigm and uses off-the-shelf SMT solvers.

We present experimental results on synthesizing a variety of bitvector
algorithms that involve unintuitive composition of
standard bitvector operations and are difficult to synthesize
manually. We also compare our technique with existing synthesis
approaches based on sketching and superoptimization.
Our tool Brahma can efficiently synthesize highly nontrivial
10-20 line loop-free programs. These programs
represent a state space of approximately 20¹⁰ programs, and
are beyond the reach of the other tools.