Component Based Synthesis Applied to Bitvector Circuits

Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan

Abstract

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 2010 programs, and

are beyond the reach of the other tools.

Details

Publication typeTechReport
NumberMSR-TR-2010-12
PublisherMicrosoft Research
> Publications > Component Based Synthesis Applied to Bitvector Circuits