  Recent advances in digital microfluidic (DMF) technologies offer a promising
platform for a wide variety of biochemical applications, such as DNA analysis,
automated drug discovery, and toxicity monitoring. For on-chip implementation
of complex bioassays, automated synthesis tools have been developed to meet the
design challenges. Currently, the synthesis tools pass through a number of
complex design steps to realize a given biochemical protocol on a target DMF
architecture. Thus, design errors can arise during the synthesis steps. Before
deploying a DMF biochip on a safety critical system, it is necessary to ensure
that the desired biochemical protocol has been correctly implemented, i.e., the
synthesized output (actuation sequences for the biochip) is free from any
design or realization errors. We propose a symbolic constraint-based analysis
framework for checking the correctness of a synthesized biochemical protocol
with respect to the original design specification. The verification scheme
based on this framework can detect several post-synthesis fluidic violations
and realization errors in 2D-array based or pin-constrained biochips as well as
in cyberphysical systems. It further generates diagnostic feedback for error
localization. We present experimental results on the polymerase chain reaction
(PCR) and in-vitro multiplexed bioassays to demonstrate the proposed
verification approach.
