Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very
many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy
various constraints. In this thesis, we demonstrate how formulations of satisfiability problems
can be used automatically to complete a design, or to find a specific design architecture that
satisfies certain constraints; how these can be used to create, debug, and optimize designs;
and introduce a domain-specific language particularly well-suited for satisfiability-assisted
design, debug, and optimization.
In the first application, we show how explicit uncertainties called â holesâ can both be natural
to use and conducive to the creation of formal satisfiability problems useful for designing
circuits. We further develop a Scala-hosted Domain Specific Language (DSL) with appropriate
syntactic sugar to make design with holes easy and effective.
We then show how, utilizing the same kind of satisfiability formulation, we can automatically
instrument a given buggy design to replace suspicious syntax fragments with potentially-correct alternatives. The satisfiability solver then determines if there is any possible set of
alternative fragments which fix the bug. We also demonstrate that this approach is reasonably
scalable, in part because there is less need for a fully-precise specification in the formulation
of the satisfiability problem.
We then advance beyond mere hole-filling and show how a tight integration of design elaboration with satisfiability solvers allows totally new approaches. To point, we use this tight
integration to create the first known methods to optimize Gate-Level Information Flow Track-
ing (GLIFT) model circuits and to make principled trade-offs in their precision.
Finally, integrating all the previous work, we propose a more powerful DSL specifically designed to address the shortcomings of the first â hole-fillingâ language. This language, which
we call Nasadiya, affords more general integrations of satisfiability into circuit design and optimization, and provides built-in modeling functionality useful for optimizing extra-functional
properties like critical path delay and circuit area. We demonstrate the utility of these features
by implementing an automatic power optimizer for a popular type of parallel prefix adders.