Search arXivSearch

arXiv · 2211.04719

A Framework for Automated Correctness Checking of Biochemical Protocol Realizations on Digital Microfluidic Biochips

Abstract

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.

Explore related subjects

Keep this discovery

BibTeXRIS

Sukanta Bhattacharjee, Ansuman Banerjee, Krishnendu Chakrabarty, Bhargab B. Bhattacharya. 2022-11-09. A Framework for Automated Correctness Checking of Biochemical Protocol Realizations on Digital Microfluidic Biochips. https://arxiv.org/abs/2211.04719

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

From Grid to Chip: Power Architecture, Stability, and Flexibility of AI Data Centers

The rapid growth of artificial intelligence (AI) computing is transforming data centers into large, dynamic electrical loads. Their deployment is primarily constrained by energy availability and grid-connection capacity, which is further aggravated by the ability of power-delivery architectures, control systems, and computing workloads to operate reliably during fast grid disturbances. This article presents a technological perspective on AI data centers as grid-interactive computing systems. First, it reviews grid-integration bottlenecks, evolving connection policies, grid-code requirements, which has fostered new technological trends via spatio-temporal flexibility available through workload orchestration, cooling systems, on-site resources, and energy storage. Second, it maps the evolution of power-delivery architectures from medium-voltage grid interfaces to chip-level, discussing higher-voltage DC distribution, solid-state transformers, wide-bandgap devices, advanced chip-level power delivery, and liquid cooling. Third, it establishes a three-level stability framework spanning rack-level DC-bus dynamics, facility-level converter interactions, and system-level grid-coupled behavior. The framework connects dominant instability mechanisms, including constant power load effects, impedance interactions, forced oscillations, and operating-mode transitions, with suitable modeling, assessment, and mitigation approaches. Synthesizing these topics, this article highlights grid-to-chip co-design as a central requirement for scalable AI infrastructure, linking computing workloads, power-delivery systems, energy buffers, and grid operation.

cs.ET

A Time-Based Readout for Vector-Matrix Multiplication in Fully Analog Memristive SNNs

Artificial neural networks rely on vector-matrix multiplications (VMMs), whose implementation in von Neumann architectures is dominated by costly data movement between memory and processing units. Spiking neural networks (SNNs) mitigate this bottleneck by performing in-memory, analog VMMs using memristive crossbar arrays. However, conventional current-mode readout circuits incur significant area and power overhead. This work proposes a fully analog readout architecture based on voltage-to-time conversion of the VMM output. By sensing the column voltage, the proposed approach avoids current-mode summing and scaling circuitry, improving area and energy efficiency. Post-layout simulations of a 10x1 SNN implemented in a 130 nm CMOS technology validate the proposed architecture, while application to a trained 64x10 SNN for digit classification further demonstrates its feasibility for SNN inference.

cs.ET

Fractional-order hardware for neuromorphic computing: Is the order really the problem?

Does a neuromorphic system need a true power-law memory kernel, and if so, can anyone build one? Neuromorphic systems process signals spanning many timescales at once, from milliseconds to tens of seconds. Integer-order circuits buy each additional timescale with an additional state variable. Fractional-order dynamics offer a different bargain: one operator whose power-law kernel carries a continuum of timescales, tuned by one parameter, the order alpha. A fractional derivative is non-local, so evaluating it costs storage and arithmetic that grow with the retained history, where an integer-order derivative costs a constant. This review organizes the hardware literature around that cost. We derive the retained history needed to hold the truncation error below a tolerance epsilon, show that it scales as epsilon^(-1/alpha), and set beside it a second and independent limit on the direct form: in fixed point the weights themselves underflow, so word length caps the usable history however long the buffer is. The two limits move at very different rates with the order, and where they cross decides whether a word length can serve an order at all. We use both to sort published hardware into three strategies, note a fourth the numerical literature has developed and this hardware has not, and survey digital, analog and device work. Along the way we ask whether the field is worried about the right obstacle. It is not. Fabricated constant-phase devices already span the orders two groups identify as task-optimal, so the order gap has largely closed, leaving a residual gap near 0.1 and at the lower order describing cortical adaptation. What remains is a frequency-band gap of about three decades at the low end. That corner is not empty, since double-layer electrodes work there, but every device in it is discrete, and no integrable thin-film element has been characterized there.

cs.ET