  Synthesis of reversible logic circuits has gained great atten- tion during
the last decade. Various synthesis techniques have been pro- posed, some
generate optimal solutions (in gate count) and are termed as exact, while
others are scalable in the sense that they can handle larger functions but
generate sub-optimal solutions. Although scalable synthe- sis is very much
essential for circuit design, exact synthesis is also of great importance as it
helps in building design library for the synthesis of larger functions. In this
paper, we propose an exact synthesis technique for re- versible circuits using
model checking. We frame the synthesis problem as a model checking instance and
propose an iterative bounded model checking calls for an optimal synthesis.
Experiments on reversible logic benchmarks shows successful synthesis of
optimal circuits. We also illus- trate optimal synthesis of random functions
with as many as 10 variables and up to 10 gates.
