MASc seminar - Murphy Thomas Reynolds Berzish

Tuesday, March 29, 2016 9:00 am - 9:00 am EDT (GMT -04:00)

Candidate

Murphy Thomas Reynolds Berzish

Title

Design of A High-Level Language and Toolchain for Microfluidic Design Automation

Supervisor

Derek Rayside

Abstract

Microfluidic circuits are currently designed by hand, using a combination of the designer's domain knowledge and educated intuition to determine unknown design parameters. Circuits are typically tested by physically constructing them in silico and performing another design iteration if issues are identified with the device.

Similar to how electronic design automation tools revolutionized the digital circuit design process, so too do microfluidic design packages have the potential to increase productivity for microfluidic circuit designers and allow more complex devices to be designed. Two of the primary software engineering problems to be solved relate to design entry and design synthesis. The circuit designer requires a programming language to describe the behaviour and properties of the device they wish to build, and a toolchain to convert this description into a model that can then be processed by other software tools. Once such a model is constructed, the remaining portions of the design toolchain must work with this model to produce a specification. The software tool must be able to find unknown design parameters automatically in order to relieve the burden of complexity placed on the designer. Furthermore, automated testing and verification tools can be used to simulate the device and check that the requirements and safety properties are met.

I outline the design of a new high-level language, Manifold, and associated compiler framework. The Manifold language is a concurrent functional systems description language suitable for modelling not only microfluidic circuits, but general physical systems. The high-level language compiler translates a system description to a domain-agnostic intermediate representation, which is then passed to a domain-specific backend for simulation, verification, and target output.

I also describe a case study in which the Manifold toolchain is applied to the problem of microfluidic design synthesis. The process involved in taking a circuit description from design entry to device specification has a number of significant steps, which I discuss in detail with respect to the design of a multi-way droplet generator circuit. The design of such a circuit is difficult for several reasons. First, the droplet generators themselves relate to the design parameter, the droplet volume, by a non-linear set of equations. The form of the equations means finding an exact solution is very difficult. Recent advances in constraint solvers which can reason about non-linear equations over real-valued terms make it possible to solve these equations efficiently and synthesize specifications that meet a given set of design constraints and goals.

Second, multiple droplet generators on the same device may interact with each other, changing the flow rates in another part of the circuit when a droplet is formed elsewhere. To address this problem, I analyze a solution which involves introducing passive regulators to critical areas of the circuit in order to control the flow rates. The properties of these regulators must be designed and then verified to ensure that they behave appropriately in the circuit. I introduce an application of a bounded model checker for safety property verification over real-valued differential equations. The model checker operates in a loop that follows a concept in formal methods known as "abstraction refinement", in which successively more detailed models are checked and a failure in one step can re-invoke a previous step with new information. In this way it is possible for the synthesis tool to perform iterations on the design while preventing itself from considering similar solutions multiple times after they have been shown to be infeasible.

The combination of the Manifold high-level language and microfluidics backend introduces a new design automation toolchain that demonstrates the effectiveness of constraint solvers in the tasks of design synthesis and verification. Further enhancements to the performance and capabilities of these solvers, as well as to the high-level language and backend, will in the future produce a general-purpose design package for microfluidic circuits that will allow for new, complex designs to be created and checked with confidence.