Cover Image

FormalRTL: Verified RTL Synthesis at Scale

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Li, Kezhi, Li, Min, Wen, Xiangyu, Zhao, Shibo, Wu, Jieying, Huang, Junhua, Xu, Qiang
Format:	Preprint
Published:	2026
Subjects:	Hardware Architecture Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Using LLMs to Facilitate Formal Verification of RTL
by: Orenes-Vera, Marcelo, et al.
Published: (2023)

IncreRTL: Traceability-Guided Incremental RTL Generation under Requirement Evolution
by: Chen, Luanrong, et al.
Published: (2026)

MEIC: Re-thinking RTL Debug Automation using LLMs
by: Xu, Ke, et al.
Published: (2024)

UVMarvel: an Automated LLM-aided UVM Machine for Subsystem-level RTL Verification
by: Ye, Junhao, et al.
Published: (2026)

RTLRewriter: Methodologies for Large Models aided RTL Code Optimization
by: Yao, Xufeng, et al.
Published: (2024)

RTLSquad: Multi-Agent Based Interpretable RTL Design
by: Wang, Bowei, et al.
Published: (2025)

Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
by: Liu, Jiale, et al.
Published: (2026)

EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR
by: Zhu, Jiaying, et al.
Published: (2026)

Synthesis-in-the-Loop Evaluation of LLMs for RTL Generation: Quality, Reliability, and Failure Modes
by: Fu, Weimin, et al.
Published: (2026)

AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
by: Zhou, Xiaofeng, et al.
Published: (2026)

A Novel HDL Code Generator for Effectively Testing FPGA Logic Synthesis Compilers
by: Xu, Zhihao, et al.
Published: (2024)

Structural Mutation Based Differential Testing for FPGA Logic Synthesis Compilers
by: Xu, Zhihao, et al.
Published: (2025)

FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols
by: Shih, Yu-An, et al.
Published: (2025)

Zero-Shot RTL Code Generation with Attention Sink Augmented Large Language Models
by: Sandal, Selim, et al.
Published: (2024)

VeriCoder: Enhancing LLM-Based RTL Code Generation through Functional Correctness Validation
by: Wei, Anjiang, et al.
Published: (2025)

OpenLLM-RTL: Open Dataset and Benchmark for LLM-Aided Design RTL Generation
by: Liu, Shang, et al.
Published: (2025)

ROVER: RTL Optimization via Verified E-Graph Rewriting
by: Coward, Samuel, et al.
Published: (2024)

PipeRTL: Timing-Aware Pipeline Optimization at IR-Level for RTL Generation
by: Yin, Shuo, et al.
Published: (2026)

GSIM: Accelerating RTL Simulation for Large-Scale Designs
by: Chen, Lu, et al.
Published: (2025)

Selective Parallel Loading of Large-Scale Compressed Graphs with ParaGrapher
by: Esfahani, Mohsen Koohi, et al.
Published: (2024)

DeepRTL2: A Versatile Model for RTL-Related Tasks
by: Liu, Yi, et al.
Published: (2025)

A Semi-Formal Verification Methodology for Efficient Configuration Coverage of Highly Configurable Digital Designs
by: Kumar, Aman, et al.
Published: (2024)

RTL-Repo: A Benchmark for Evaluating LLMs on Large-Scale RTL Design Projects
by: Allam, Ahmed, et al.
Published: (2024)

FVRuleLearner: Operator-Level Reasoning Tree (OP-Tree)-Based Rules Learning for Formal Verification
by: Wan, Lily Jiaxin, et al.
Published: (2026)

ITHICA: Intra-Thread Instruction Checking Approach for Defect-Induced Silent Data Corruptions
by: Vavelidou, Ioanna, et al.
Published: (2026)

Quantifying Uncertainty in FMEDA Safety Metrics: An Error Propagation Approach for Enhanced ASIC Verification
by: Armato, Antonino, et al.
Published: (2026)

LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
by: Miao, Mingkai, et al.
Published: (2026)

Offloading Data Center Tax
by: Revankar, Akshay, et al.
Published: (2025)

C2HLSC: Leveraging Large Language Models to Bridge the Software-to-Hardware Design Gap
by: Collini, Luca, et al.
Published: (2024)

A Vertically Integrated Framework for Templatized Chip Design
by: Kim, Jeongeun, et al.
Published: (2025)

Scalable Software Testing in Fast Virtual Platforms: Leveraging SystemC, QEMU and Containerization
by: Jünger, Lukas, et al.
Published: (2025)

ScaleRTL: Scaling LLMs with Reasoning Data and Test-Time Compute for Accurate RTL Code Generation
by: Deng, Chenhui, et al.
Published: (2025)

VFocus: Better Verilog Generation from Large Language Model via Focused Reasoning
by: Zhao, Zhuorui, et al.
Published: (2025)

A High-level Synthesis Toolchain for the Julia Language
by: Short, Benedict, et al.
Published: (2025)

Extend IVerilog to Support Batch RTL Fault Simulation
by: Tang, Jiaping, et al.
Published: (2025)

SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
by: Chang, Fu-Chieh, et al.
Published: (2026)

AnalogXpert: Automating Analog Topology Synthesis by Incorporating Circuit Design Expertise into Large Language Models
by: Zhang, Haoyi, et al.
Published: (2024)

ACE-RTL: When Agentic Context Evolution Meets RTL-Specialized LLMs
by: Deng, Chenhui, et al.
Published: (2026)

SmaRTLy: RTL Optimization with Logic Inferencing and Structural Rebuilding
by: Li, Chengxi, et al.
Published: (2025)

GreenMalloc: Allocator Optimisation for Industrial Workloads
by: Dakhama, Aidan, et al.
Published: (2025)