Automated Generation of RISC-V Extensions with Formal Correctness Guarantees

All Your Assembly Belongs to Rust: Automated Lifting for Uniform Testing and Verification

This paper translates Rust code containing RISC-V inline assembly into pure Rust code by emulating each instruction using a machine model extracted from the official RISC-V Sail ISA specification, and demonstrates how each category is handled by the translation.

Quantifying the Code-Size Overhead of eBPF JIT Compilation

eBPF allows user-defined programs to safely extend Linux kernel functionality at runtime, but its final machine code comes from a compilation pipeline that differs from native targets, and how efficient that pipeline is has no clear reference point. Our work constructs one: using the standard LLVM x86 backend as an approximate best case for code-generation quality, we compile nearly identical source through both the eBPF path (with kernel JIT) and a native path. We hold source logic, optimization level, and build configuration equal, so the two differ only in their backend target and can be compared fairly by code size. Applying this to Cilium datapath programs, the two pipelines stay nearly identical through the frontend and midend, which isolates the overhead almost entirely to backend code generation, where the eBPF output contains 27.6% more instructions and is 16.6% larger in bytes. The baseline then lets us attribute the gap to a few recurring causes (operand widening, address computation, memory copies, register pressure) and categorize each by root cause, as coming from the eBPF instruction set or from a less mature backend, or a mix of both. This pinpoints where the overhead occurs and provides a method to measure it for other eBPF workloads and backends. Because eBPF code runs in hot kernel paths, this overhead is worth reducing, and the baseline offers a stable reference for measuring how far eBPF code generation is from native quality and tracking that gap as backends mature, for other projects and workloads.

Unifying eBPF across Platforms: Formal Semantics, Conformance Testing, and Specifications

eBPF is no longer a single-platform technology. It runs in the Linux kernel, on Windows, in user space, on microcontrollers, and in blockchain virtual machines, on independently built runtimes. The IETF ISA standard, RFC 9669, pins down the core instructions but leaves out features that real programs depend on, such as helper functions and maps. We are building an executable formal semantics for eBPF in F* that explicitly distinguishes cross-platform and platform-specific behaviors. Our semantics passes the BPF conformance test suite on par with uBPF, bpftime, Linux, and Windows, and we are extending it beyond the core ISA to other shared features the RFC omits. Using Meta-F* metaprogramming, we can also generate prose specifications in structured English that provably match the model. We envision this semantics as a practical foundation for a uniform, trustworthy eBPF across platforms.

A Compilation-based Under-Constrained Execution Engine

PerfReasoning: How Well Do LLMs Reason on Hardware Performance?

Performance modeling is central to hardware design and software optimization, yet constructing these models requires structured reasoning about computation, data reuse, storage, and movement. We introduce PerfReasoning, a benchmark that evaluates LLMs both as direct performance reasoners and as generators of analytical performance-model code. Given workload, architecture, and mapping specifications, models compare mappings and predict off-chip traffic and buffer requirements. The strongest closed-source models exceed 90% on reasoning-based Q&A, and the best open-weight model reaches 82.4%. However, model construction is substantially harder: while GPT-5.6 Sol exceeds 80% pass rate, all other model configurations average below 45% and vary markedly across runs. Task-specific RL raises a 4B model's mapping-reasoning accuracy by 15.7 points, whereas feedback-free multi-round self-revision prompting is not reliably effective. PerfReasoning exposes the gap between plausible architectural reasoning and reliable performance-model construction. We will publicly release the benchmark to support reproducible evaluation and track future progress.

Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations

Large language models (LLMs) are increasingly being explored for automating SystemVerilog Assertion (SVA) generation, yet most evaluations report correctness on a single syntactic representation of an input. Such point accuracy does not reveal whether a model's correct output is stable when the same RTL behavior is written differently. This paper presents a controlled metamorphic evaluation of LLM-based SVA generation under semantics-preserving RTL transformations. Starting from the VERT dataset, we construct a quality-filtered conditional-control pool and a stratified 40-program evaluation set containing 295 assignment behaviors. We evaluate two open code models, Qwen2.5-Coder-7B and DeepSeek-Coder-V2-Lite, with an identical evaluation prompt and greedy decoding. Three transformations are studied: operand reordering, deterministic identifier renaming, and redundant parenthesization. Beyond baseline and transformed accuracy, we measure conditional robustness, invariance failure, and any-flip rate, with 10,000-sample clustered bootstrap intervals at the RTL-program level. Across all six model-transformation conditions, 9.7%-27.0% of behaviors that were correct on the original RTL become incorrect after a semantics-preserving transformation. Aggregate accuracy can therefore hide substantial instability: under identifier renaming, DeepSeek-Coder-V2-Lite improves from 53.9% to 63.7% accuracy while 19.5% of its originally correct behaviors fail. Manual review of 30 sampled correct-to-wrong transitions identifies dropped path predicates, branch-polarity errors, Boolean-structure corruption, and output-contract violations. The results show that point accuracy alone is insufficient for characterizing LLM reliability in assertion generation and motivate robustness-aware evaluation for AI-assisted hardware verification.