Functional Analysis of Large-scale DNA Strand Displacement Circuits

We present a method for the analysis of functional properties of large-scale DNA strand displacement (DSD) circuits based on Satisfiability Modulo Theories that enables us to prove the functional correctness of DNA circuit designs for arbitrary inputs, and provides significantly improved scalability and expressivity over existing methods. We implement this method as an extension to the Visual DSD tool, and use it to formalize the behavior of a 4-bit square root circuit, together with the components used for its construction. We show that our method successfully verifies that certain designs function as required and identifies erroneous computations in others, even when millions of copies of a circuit are interacting with each other in parallel. Our method is also applicable in the verification of properties for more general chemical reaction networks.