Synthesis of Microfluidic Chip Designs using SMT Solvers

点击翻译按钮获取中文摘要

Microfluidic chips, lab-on-a-chip devices that have channels transporting liquids instead of wires carrying electrons, have attracted considerable attention recently from the bio-medical industry because of their application in testing assay and large-scale chemical reaction automation. These chips promise dramatic reduction in the cost of large-scale reactions and bio-chemical sensors. The market for microfluidics is estimated to grow to over $10B in the duration of this grant. As in computer chip design, there is an acute need for automation tools that can assist with design, testing and verification of microfluidic chips. The current state of practice is that microfluidics chips are designed manually using a guess-and-check approach. Typically a designer will select design parameters based on experience, and then code a simulation in Matlab, COMSOL, or a similar tool. If the simulation succeeds, then a prototype chip might be built for physical testing. This state of affairs is exacerbated by the reality that a microfluidic chip design must consider a wide variety of physical properties, potentially including fluid, pressure, spatial, electrical, thermal, and optical. If the designer makes an error or omission on any one of these dimensions then the design might not work as intended. We propose a design methodology for microfluidic chips based on SMT solvers, with the goal of producing designs that are correct by construction. (At least correct with respect to the mathematical models that are used to describe the design; as in other areas of engineering, these models are sometimes imperfect representations of physical reality.) The chip designer will specify known values, such as the location of wells or certain activation voltages, and then the system will solve for the other design parameters (such as the pull-back voltages). Recently, CMU has developed dReal: an SMT solver for nonlinear multi-variate inequalities over the reals. We have constructed proof-of-concept prototypes with dReal to demonstrate that it can be used for microfluidic chip design. We intend to develop high-level hardware description languages for microfluidic circuits, and a computational framework based on CEGAR (Counter-Example Guided Abstraction Refinement), using Reduced Order Models as the starting point. This proposal comprises 7 graduate students: 2 PhD + 5 MASc 1 PhD co-supervised with Abukhdeir (computational fluid dynamics) 1 MASc co-supervised with Ren & Backhouse (microfluidics) 1 MASc co-supervised with Kennings (electronic design automation) Microfluidic chip design is exceedingly complex. There is a great need for design automation tools. Recent advances in SMT solvers make them applicable to these problems. We propose to use (and enhance) these solvers to create microfluidic design tools that help chip designers produce designs that are correct by construction.