Abstract
With the advances of the micro uidic technology, the design of digital micro uidic biochips recently received signicant attention. But thus far, the corresponding design tasks such as binding, scheduling, placement, and routing have usually been considered separately. Furthermore, often just heuris-tic results have been obtained. In this work, we present a one-pass synthesis scheme which directly realizes the desired functionality onto the chip and, at the same time, guaran-tees minimality with respect to area and/or timing. For this purpose, the deductive power of solvers for Boolean satis-ability is exploited. Experiments show how the approach leverages the design of the respective devices. Copyright 2014 ACM.