Automated hardware synthesis from formal specification using SAT solvers

System and circuit design can be considered as planning problems, where resources are deployed in time and space to meet a given goal. Recent and continuing developments in the size of SAT problems and other AR problems that can be solved with off-the-shelf tools leads us to consider their direct use in system design. In this paper, we start to tackle the design of small hardware subsystems and the generation of glue logic between systems by asking a SAT solver to generate the programming bit stream for a fictional gate array.