Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2009.03242

PolyAdd: Polynomial Formal Verification of Adder Circuits

Rolf Drechsler
View original source ↗Read source document ↗Export metadata ↓

Abstract

Only by formal verification approaches functional correctness can be ensured. While for many circuits fast verification is possible, in other cases the approaches fail. In general no efficient algorithms can be given, since the underlying verification problem is NP-complete. In this paper we prove that for different types of adder circuits polynomial verification can be ensured based on BDDs. While it is known that the output functions for addition are polynomially bounded, we show in the following that the entire construction process can be carried out in polynomial time. This is shown for the simple Ripple Carry Adder, but also for fast adders like the Conditional Sum Adder and the Carry Look Ahead Adder. Properties about the adder function are proven and the core principle of polynomial verification is described that can also be extended to other classes of functions and circuit realizations.

Explore related subjects

cs.ARcs.DScs.SC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Rolf Drechsler. 2021-04-03. PolyAdd: Polynomial Formal Verification of Adder Circuits. https://arxiv.org/abs/2009.03242

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

KEEP EXPLORING

Related papers

arXiv2026

PipeDRAM: A Data-Transposition-Free In-DRAM Architecture with Hardware/Software Pipelining

Processing-using-DRAM (PUD) architectures exploit the analog operational properties of DRAM to perform bulk bitwise Boolean and arithmetic operations inside memory arrays by organizing data in a vertical layout, where operand bits are stacked along DRAM columns. However, modern computing systems natively employ a horizontal data layout that preserves the cache line abstraction, leverages spatial locality in row buffers, and enables high memory throughput. This fundamental mismatch forces existing PUD architectures to frequently perform data layout transformations between horizontal and vertical formats, incurring significant performance, energy, and system integration overheads. Our goal is to eliminate data transposition overheads in PUD systems at low cost. To this end, we propose PipeDRAM, a PUD architecture that eliminates the need for runtime data layout transformation, enabling PUD operations directly over horizontally laid-out data. PipeDRAM's key ideas are to (i) deterministically reorganize bits inside each memory request to enable a PUD-friendly data placement within a DRAM array in a horizontal data layout, and (ii) employ a pipeline-based execution model that overlaps bit-dependent and bit-independent in-DRAM operations to exploit bit-level parallelism across the memory array. We compare PipeDRAM to different computing platforms. PipeDRAM provides (i) 11.8x, 11.8x, and 80.4x higher performance and (ii) 25.4x, 3.0x, and 38.0x lower energy consumption than three state-of-the-art PUD systems. PipeDRAM incurs low area cost on top of a DRAM chip (1.86%) and CPU die (0.05%). To enable further research on PUD systems, we open-source PipeDRAM at https://github.com/CMU-SAFARI/PipeDRAM.

cs.AR↗
arXiv2026

Implementation and Evaluation of NTT Arithmetic for ML-KEM on a CGLA

FIPS 203 standardizes ML-KEM for post-quantum key establishment. Its polynomial multiplication relies on NTT butterflies with exact modular arithmetic over q = 3329. Dedicated NTT accelerators minimize latency with fixed modular arithmetic and stage schedules. A CPU-Grounded Linear Array (CGLA) reuses one programmable linear datapath across several workloads. Mapping the transform to this datapath requires exact FP32 reconstruction and explicit stage transitions across the ARM-to-CGLA interface. We implement an eight-stage cyclic radix-2 driver over the ML-KEM modulus by splitting each twiddle into 8-bit and 4-bit parts before modular reduction. This driver differs from the standardized seven-layer incomplete negacyclic NTT and does not implement the full ML-KEM polynomial multiplication path. The arithmetic sequence keeps every integer below 2^24. One 41-PE call fuses the first two radix-2 stages, and six 47-PE calls execute the remaining stages while scattering outputs into next-stage records. Across four cohorts, 105 FPGA runs match all 817152 output coefficients. At batch size 64, measured FPGA end-to-end latency is 27.5 us per NTT, and the ASIC projection is 6.74 us. With PE gating, projected ASIC system energy is 10.1 uJ per NTT at batch size 8 and 58.9 uJ at batch size 64.

cs.AR↗
arXiv2026

HBF-Sim: An Extensible HBF Simulator for Large-scale GPU Memory Systems

High-bandwidth flash (HBF) is introduced to address the memory wall, which can co-package a dense NAND stack with the GPU, targeting the performance gap between near-accelerator bandwidth and flash density. HBF, however, is neither a large HBM nor a fast NVMe SSD. Its usable bandwidth depends on how GPU cache-line requests map onto NAND pages, how concurrency spreads across channel-affine die sets, and how media management interacts with the GPU memory pipeline. To our knowledge, existing GPU, SSD, or HBF simulators cannot faithfully model this behavior. We present HBF-Sim, an extensible, reusable, and faithful HBF simulator integrated with simulated GPUs. It closes the loop between GPU issue limits, device queuing, and NAND behavior in one end-to-end request path. HBF-Sim separates a GPU-HBF interaction controller from page-based parallel stack storage, and it models the full GPU-HBF request path. It provides an MSHR-based address mapping table that merges cache-line requests into page-based operations, as well as a page-based multi-stack flash manager for highly parallel reads and writes. Validation tests and device-level microbenchmarks expose performance bottlenecks caused by limited channel distribution and resource conflicts, offering concrete guidance for next-generation HBF architectures.

cs.AR↗