Synthesis of Microfluidic Chip Designs using SMT Solvers

使用 SMT 求解器综合微流控芯片设计

• 批准号: RGPIN-2015-06203
• 负责人: Rayside, Derek
• 金额: $ 1.75万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2018
• 资助国家: 加拿大
• 起止时间: 2018-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=663080
• 关键词: Synthesis; Microfluidic; Chip; Designs; using

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. **

微流控芯片是一种具有传输液体的通道而不是携带电子的导线的芯片上实验室设备，由于其在测试分析和大规模化学反应自动化中的应用，近年来引起了生物医学行业的极大关注。这些芯片有望大幅降低大规模反应和生化传感器的成本。微流体市场估计将增长到超过100亿美元在此期间授予。*在计算机芯片设计中，迫切需要能够帮助设计、测试和验证微流控芯片的自动化工具。 目前的实践状态是，微流体芯片是使用猜测和检查方法手动设计的。 通常，设计人员将根据经验选择设计参数，然后在Matlab、COMSOL或类似工具中编写仿真代码。如果模拟成功，那么可能会构建原型芯片进行物理测试。这种状况由于微流体芯片设计必须考虑各种物理性质的现实而加剧，这些物理性质可能包括流体、压力、空间、电、热和光学。 如果设计者在这些尺寸中的任何一个上犯了错误或遗漏，那么设计可能无法按预期工作。我们提出了一种基于SMT求解器的微流控芯片的设计方法，其目标是通过构造来产生正确的设计。(At（在描述设计的数学模型方面，这些模型最不正确;与其他工程领域一样，这些模型有时对物理现实的描述并不完美。芯片设计者将指定已知值，例如威尔斯的位置或某些激活电压，然后系统将求解其他设计参数（例如回拉电压）。最近，CMU开发了dReal：实域上非线性多变量不等式的SMT求解器。 我们已经用dReal构建了概念验证原型，以证明它可以用于微流控芯片设计。** 我们打算开发用于微流体电路的高级硬件描述语言，以及基于CEGAR（反例引导抽象细化）的计算框架，使用降阶模型作为起点。该提案由7名研究生组成：2名博士+ 5名MASc*1名博士与Abukhdeir（计算流体动力学）共同监督 *1名MASc与Ren & Backhouse（微流体学）共同监督 *1名MASc与Kennings（电子设计自动化）共同监督 ** 微流体芯片设计非常复杂。设计自动化工具的需求很大。SMT求解器的最新进展使其适用于这些问题。我们建议使用（并增强）这些求解器来创建微流体设计工具，以帮助芯片设计人员制作正确的设计。**