Component Based Synthesis Applied to Bitvector Circuits - Gulwani, Sumit; Venkatesan, Ramarathnam (Microsoft Research, 2009)
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.