Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1406.1565

Modeling Algorithms in SystemC and ACL2

John W. O'Leary·David M. Russinoff
View original source ↗Read source document ↗Export metadata ↓

Abstract

We describe the formal language MASC, based on a subset of SystemC and intended for modeling algorithms to be implemented in hardware. By means of a special-purpose parser, an algorithm coded in SystemC is converted to a MASC model for the purpose of documentation, which in turn is translated to ACL2 for formal verification. The parser also generates a SystemC variant that is suitable as input to a high-level synthesis tool. As an illustration of this methodology, we describe a proof of correctness of a simple 32-bit radix-4 multiplier.

Explore related subjects

cs.ARcs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

John W. O'Leary, David M. Russinoff. 2014-06-06. Modeling Algorithms in SystemC and ACL2. https://doi.org/10.4204/eptcs.152.12

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

KEEP EXPLORING

Related papers

arXiv2026

Implementation of an Adaptive Transformer Accelerator for Accurate Outdoor Localization with Massive MIMO

We present a sparsity-aware FPGA implementation of an adaptive Transformer-based localization accelerator for 5G massive MIMO targeting sub-10\,ms real-time positioning. The architecture exploits propagation characteristics, where beam-delay channel representations exhibit sparsity, enabling a row-wise skipping mechanism that removes low-energy beam components with minimal control overhead. Transformer computations are mapped onto a heterogeneous vector processing engine with parallel processing elements and adder trees, using mixed input- and output-stationary dataflow execution for efficient matrix computation and reduced data movement. Environment-dependent processing is supported through a lightweight runtime model-switching mechanism, where temporally filtered outputs of a single-layer perceptron router enable selection between specialized models with reduced latency. Implemented on a Xilinx Zynq UltraScale+ FPGA and evaluated on real-world massive MIMO measurements, the design achieves up to 65\% row sparsity, yielding peak computational speedups of approximately 2x while limiting the average localization accuracy degradation to below 10\%, relative to the fixed-point baseline model. The accelerator attains below 1.15\,m localization accuracy across scenarios, with inference latency of 0.51-2.11\,ms and throughput of up to 1961 positions/s. These results demonstrate that propagation-aware sparsity, mixed dataflow execution, and efficient runtime model switching enable a scalable and low-latency hardware realization of adaptive Transformer-based localization for real-time 5G systems.

cs.AR↗
arXiv2026

RTLScout: Joint Agentic Code and Synthesis Optimization for Efficient Digital Circuits

We present RTLScout, an autonomous system that combines LLM-driven agentic design with logic synthesis optimization and arithmetic architecture selection. An LLM agent iteratively writes, evaluates, and refines RTL designs, guided by delay and area feedback from Yosys and OpenROAD. The agent writes Spire, a Python-embedded HDL we introduce, in which optimization intent is expressed locally in the source, selecting logic-synthesis or arithmetic-architecture optimizations per subcircuit. The four-phase pipeline relies entirely on open-source EDA tools and an open-weights LLM. On an IEEE-754-compliant 16-bit floating-point multiplier with subnormal support, RTLScout reduces area by 34% and delay by 38% relative to a starting design and outperforms a commercial-tool reference design on the ASAP7 technology. We show that agentic RTL rewriting and synthesis optimization are complementary, with neither alone reaching the result of the full pipeline. On 14 RTLRewriter benchmarks, the Spire-based pipeline achieves 16.3% lower mean per-case Yosys cell count than an otherwise identical Verilog pipeline.

cs.AR↗
arXiv2026

HBF Sucks? A Full-Stack Characterization of High-Bandwidth Flash for KV-Centric LLM Serving

A faster storage device should make serving faster. We find the opposite. High-Bandwidth Flash (HBF) stacks NAND behind a wide, package-local interface, promising flash-scale capacity with far lower read latency and higher bandwidth than an SSD. The obvious move is to keep an SSD-style Mooncake KV-offloading stack and swap in HBF underneath. We built that system and measured it: an extended TokenSim, four complete two-hour Qwen-Bailian production traces, five dense and mixture-of-experts models, and H100/B200 profiles. The upgrade backfires. Average end-to-end latency rises 2--5.5$\times$ and maximum SLO goodput falls 1.1--2.7$\times$ across H100 and B200, so the faster device yields a slower system. A cost-benefit model explains the paradox: a faster far tier pays off only when read I/O is the bottleneck, reads outweigh writes, and delivered bandwidth is sustainable. Transient KV violates all three at once. Buying flash through the package costs GPU near-tier capacity and bandwidth, while HBF's own read/write latency barely matters: scaling it 3.75$\times$ moves latency less than 1\%. Worse, the two-tier hierarchy keeps reuse in the near tier and hands HBF a relentless write-heavy stream. Writes outnumber reads on every trace, so a 3D-ICE model shows the stack hits its thermal limit well below peak bandwidth, and a TLC tier wears out sooner than the SSD pool it replaced. The device is fine; the drop-in deployment is not. HBF sucks as an SSD replacement for transient KV, but earns its place in LLM serving when used selectively with reuse-aware placement, write budgeting, and thermal coordination.

cs.AR↗