Skip to content
Preprint

SIMT-Aware Lockstep Verification and Functional-Coverage Closure Methodology for an Open-Source RISC-V GPGPU: A UVM 1.2 Environment

Sep 2026 · 0 citations · 23 references
Computer Science

TL;DR

A UVM 1.2 environment and methodology that wraps a bus-master SIMT DUT with role-inverted agents, integrates Vortex's functional simulator (SimX) as a per-configuration golden model over DPI-C, and renders verdicts via two injection-qualified checkers.

Abstract

Open-source RISC-V GPGPUs such as Vortex ship with directed-kernel regressions but no reference-model checking, functional-coverage model, or sign-off discipline. This paper presents a UVM 1.2 environment and methodology that closes that gap. The environment wraps a bus-master SIMT DUT with role-inverted agents, integrates Vortex's functional simulator (SimX) as a per-configuration golden model over DPI-C, and renders verdicts via two injection-qualified checkers: a bidirectional end-state scoreboard and a per-instruction, per-lane lockstep comparator under five SIMT alignment rules. A two-pass load-value feed makes racy fenceless multi-core programs instruction-granularity verifiable (residual zero over 5,432 retirements), with the interrupt-timing boundary stated. A three-layer coverage model adds, to our knowledge, the first published SIMT functional-coverage layer for RTL GPU verification (divergence depth, bank conflicts, coalescing classes), closing its own layers at 98.1% covergroup-bin / 94.7% total (ISA layer separately: 83.1% bins / 89.3% weighted) under machine-generated, RTL-cited exclusions and a blocking waiver-integrity gate; an unstimulated D-extension elaboration affects no functional bin, only lowering totals. The checking depth surfaced real defects on both sides of the comparison: a JALR LSB ISA deviation, a non-scaling watchdog constant (since fixed upstream), a reset-relay X window found by restoring a silenced assertion, a missing AXI error path proven by fault injection, and a reference-model fetch bug found by the lockstep itself. FuzzGPU (USENIX Security 2026), a concurrent RTL GPU fuzzer on the same DUT, is complementary: fuzzing finds bugs, this methodology quantifies sign-off; both independently found the JALR deviation. All findings ship in an evidence-cited register; every number carries provenance and the method's boundaries are stated rather than waived.

View source

Similar papers

#software testing Open access Sep 2026

LLM-Assisted Porting of Security-Critical C Libraries to Idiomatic Rust: A Multi-Model Empirical Study

Differential fuzzing reveals complementary bugs in the manual and LLM porting of security-critical C libraries to idiomatic Rust and translates these findings into concrete practical guidance for teams planning a similar migration.

Marco Parrillo, Marco Grassi, Luigi Laura · 0 citations

Automated Generation of RISC-V Extensions with Formal Correctness Guarantees

Janus is presented, an LLM-assisted framework that synthe-sizes custom instructions integrated into the Ibex RISC-V core while keeping correctness outside the agent, demonstrating a practical path for using LLMs to explore ISA specialization without making the agent part of the trusted correctness boundary.

Elisavet Lydia Alvanaki, Jia-Kun Wang, Eugenio Muscinelli et al. · 0 citations
Preprint Sep 2026

SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification

This work identifies two recurring proof barriers in self-composed IFV: implementation complexity, where proof-hard datapath logic dominates even though the property needs only a compact boundary relation, and relational inductive complexity, where the proof depends on cross-copy public-control facts that the backend p...

Liangtao Dai, Yimin Gao, Melika Morsali et al. · 0 citations
Preprint Sep 2026

VSpector: Specification-Driven Bug Detection for RISC-V CPUs

VSpector is presented, a specification-driven bug detection pipeline that directly checks whether CPU register-transfer level (RTL) implementations adhere to official specification rules, without requiring specialized construction of reference models, formal properties, or custom bug patterns.

Tian-Yu Jia, Zhao-Yang Yu, Yuan-Liang Chen et al. · 0 citations
Open access 2026

Deployment-Oriented Evaluation of LLM-Generated Optimization Code: Repairability, Compatibility, and Constraint-Coverage in Parallel-Machine Scheduling

Large language models (LLMs) increasingly generate executable optimization code, yet evaluations often rank programs by objective value, overlooking deployment-relevant properties such as validity under structural constraint changes, failure localization, repairability, and component compatibility. We introduce GenSE-S...

Achraf Ghorbel, Nourchène Elleuch Ben Ayed, Keletso J. Letsholo et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.