Skip to content
Review

Spec-Driven Hardware Evolution via Executable Contract Refinement and Proof-Guided RTL Update

Aug 2026 · 0 citations · 43 references
Computer Science

TL;DR

The results support the feasibility of contract-driven hardware evolution and demonstrate that the proposed backend workflow can effectively drive validated legacy RTL toward next-version functional convergence under a reviewed executable contract.

Abstract

Hardware development is inherently evolutionary: major revisions typically begin by changing intended behavior and then updating a previously validated implementation, rather than regenerating RTL from scratch. Yet most recent LLM-based hardware research still frames the task primarily as prompt-to-RTL generation, offering limited support for semantic version evolution of trusted legacy designs. We present spec-driven hardware evolution, a contract-centered formulation for RTL version iteration. Instead of treating a new feature request as a direct prompt for RTL generation, we refine it into a reviewed executable contract for the next version. This contract specifies what must hold at the externally visible transactional level through a behavior-level reference together with explicit observation and checking semantics, while leaving how the change is realized in RTL to the evolution process. Based on this formulation, we organize hardware evolution into four stages: Specify, Plan, Implement, and Validate. After contract approval, the remaining stages proceed automatically: Plan derives cross-version semantic deltas and localizes affected RTL regions, aided by mutation-based semantic probing; Implement and Validate then perform legacy-aware RTL update under proof-guided checking and iterative repair. We evaluate the framework on a controlled version-evolution case study of a representative TPU datapath block under data-format changes. The results support the feasibility of contract-driven hardware evolution and demonstrate that the proposed backend workflow can effectively drive validated legacy RTL toward next-version functional convergence under a reviewed executable contract. An anonymous artifact for reproducibility is available at https://anonymous.4open.science/r/SDHE-3A6C.

View source

Similar papers

Conference Open access Sep 2026

QiMeng-VPID: Verification-Grounded Port-Level Iterative Decomposition for Complex Verilog Generation

This work proposes VPID, a multi-agent framework for generating complex Verilog that achieves monotonic functional improvement and introduces an experience-guided refinement strategy that distills historical waveform mismatches into constraints, guiding the targeted debugging for the unverified ports.

Hong-Guang Wang, Jiaming Guo, Rui Zhang et al. · 0 citations
Open access Sep 2026

From Formal Specifications to Simulations: Generating Executable Hardware Models for Early Validation

Formal specification techniques have been introduced to address the ambiguities inherent in natural-language hardware specifications. One such approach is the Universal Specification Format (USF), which provides a machine-readable, formal reference for Register-Transfer Level (RTL) verification. However, verifying agai...

Robert Kunzelmann, Raphael Kunz, Stephanie Ecker et al. · 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
#artificial intelligence Preprint Sep 2026

Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization

The upgrade and rewriting of large scientific codebases has traditionally been a major challenge. While evolutionary search with large language models (LLMs) can port and accelerate legacy code, repair feedback in prompts alone does not prevent subsequent candidates from repeating the same errors. We introduce Certific...

Piyush Jha, A. Ghosh, Vijay Ganesh · 0 citations
Review Aug 2026

OSFoundry: Building and Evolving Operating Systems with Specification-Guided Agents

Operating systems must evolve continuously. Yet their development remains code-centric and largely manual: even a localized change can require recovering implicit assumptions, coordinating multiple subsystems, and repeatedly building, booting, testing, and debugging the complete system. General-purpose coding agents au...

Heng Zhang, Qing-Yuan Liu, Mo Zou 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.