The paper describes a universal approach to formal verification of modular multipliers and other modular arithmetic circuits. It is based on a hardware system that reverses modular reduction of $X=A \cdot B$, subtracts the remainder $R$, and divides $X-R$ by modulus $m$. In a correct modular reduction circuit, this division should yield a zero remainder $R_{m}$. Verification reduces to checking if every bit of $R_{m}$ is zero. The verification system is constructed from pre-verified arithmetic components (multiplier and divider) and synthesized using standard optimization tools such as Yosys and ABC. The method applies to any modular reduction circuit, regardless of its structure, operand width, or modulus value. We tested the method on various modular multiplier types, including large modulo $\left(2^{n}+1\right)$ multipliers and Barrett multipliers with different operand and modulus sizes, showing promising results. To the best of our knowledge, such a method has not been proposed before. Except for structured modulo $\left(2^{n}+1\right)$ multipliers, no suitable reference was found for comparison.
With phenomenal progress in SAT solvers, Bounded Model Checking (BMC) tools have grown in prominence today. A popular and important line of research in the domain of SAT Solvers is efficient Learnt Clause Management (LCM). Clauses are learnt through conflicts during SAT solving which are crucial for pruning the search space, hence reducing runtime. Most solvers usually keep an upper bound on the number of learnt clauses to be retained as too many redundant clauses can slow it down. Hence, it becomes imperative to determine the comparative importance of the learnt clauses. One of the popular metrics to evaluate this relative importance in the SAT solver parlance is the Literal Block Distance (LBD). Our paper extends this metric of clause importance to the BMC context. In this paper, we present a novel mechanism based on the incremental nature of BMC to predict the importance of learnt clauses across future BMC iterations. We use it to propose a new LCM policy and integrate it with the LBD based technique. The motivation for this work stems from the fact that the expense of generating (not solving) the SAT formula of the future BMC iterations is minimal but it can give a lot of insight about which learnt clauses to retain. Experiments on HWMCC benchmarks show comparable or improved results for 89 % of the benchmarks on average.
This work proposes a vertical fixed pattern noise (VFPN) reduction technique in CMOS image sensors. The technique incorporates the use of double sampling circuit wherein the offset voltage of the amplifier is stored during the sampling phase and canceled in the amplification phase without any increment in chip area and clock cycles. The proposed technique is implemented as a column-parallel readout with the pitch of 9 µm and verified over silicon for a 128 × 96 pixel array. The measurement results show the reduction in vertical FPN to 0.069%. The prototype image sensor is designed and fabricated in AMS 350 nm CMOS OPTO process using 3.3 V power supply. The designed image sensor occupies an area of 1.69 mm × 5.75 mm and consumes 55 mW of power.
This paper introduces an intelligent digital microfluidic biochip (DMFB) system that integrates deep learning for automated droplet manipulation with an intuitive interface for manual control. Our approach combines a custom, low-cost $8 \times 8$ electrode array fabricated on a printed circuit board (PCB) with a real-time vision system. The system utilizes copper-coated electrodes with cost-effective dielectric and hydrophobic layers, driven by a microcontroller-based high-voltage actuation circuit. Real-time, autonomous droplet manipulation is enabled by a deep learning-based pipeline that features a fine-tuned You Only Look Once (YOLOv11n) model for robust droplet detection and an intelligent routing algorithm for generating optimal, collision-free routing paths. Experimental validation demonstrates high system performance, with the automation pipeline achieving a 90% routing success rate and the YOLOv11n detector attaining a mean Average Precision (mAP@0.5) of 0.993 on a custom-created dataset. Furthermore, the system incorporates a graphical user interface (GUI) for manual control, which exhibited 98% task accuracy. By successfully integrating affordable hardware with advanced computer vision, this work presents a scalable and accessible platform for automated biochemical assays, demonstrating significant potential to advance applications in point-of-care diagnostics, drug discovery, and personalized medicine.
The memory wall problem significantly hampers the performance of modern data-intensive applications (such as AI/ML) in conventional computing architectures. Near-Memory Computing (NMC) offers a promising alternative by embedding computation units within main memory; however, it necessitates an effective offloading approach. Current offloading approaches primarily concentrate on performance metrics, often neglecting energy considerations during decision-making. Furthermore, many existing approaches require conducting preliminary trials on both the host and NMC sides, which can lead to considerable overhead. To address these challenges, we propose EP-Off, an estimation-based dynamic offloading approach. Initially, EP-Off executes a few iterations of the offloadable region exclusively on the host CPU, allowing for the estimation of the Energy-Delay Product (EDP) for both host and NMC sides. The remaining portion is then offloaded to the side with the lower estimated EDP. This approach ensures a well-balanced decision-making process that strikes a balance between performance and energy efficiency, while reducing overhead by eliminating unnecessary preliminary trials on the NMC. Through extensive experiments with diverse data-intensive applications, EP-Off exhibits substantial performance improvements ($2.1 x$ & $1.5 x$), energy saving (54% & 35%), and reductions in off-chip data transfers (65% & 27%) compared to both conventional and state-of-the-art approaches. Furthermore, EP-Off reduces EDP by 79% and 52% compared to conventional and state-of-the-art approaches, respectively.
