AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs

• URL: http://arxiv.org/abs/2604.22285v1
• Date: Fri, 24 Apr 2026 07:02:58 GMT
• Title: AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
• Abstract summary: High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction into a register-transfer level (RTL) design.<n>HLS may contain major functional bugs or security vulnerabilities due to limitations or errors in the tools.<n>We propose utilizing the high-level design features from the HLS flow to construct a set of helper assertions aimed at guiding the model checker.
• Score: 5.472549507568446
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced development time and greater flexibility in design space exploration. However, such machine-generated RTL designs may contain major functional bugs or security vulnerabilities due to limitations or errors in the HLS tools. One of the most reliable methods to identify these vulnerabilities is formal verification, particularly model checking. Nevertheless, the large size of the generated RTL often causes model checking to struggle to conclude within reasonable time or resource limits. In this study, we propose utilizing the high-level design features from the HLS flow to construct a set of helper assertions aimed at guiding the model checker and accelerating the verification process. To identify the most effective set of helpers to assist the model checker, we develop a proving mechanism that iteratively reuses proving information to select the potentially most useful set of helpers. We evaluate the proposed framework on a set of HLS design benchmarks. Experimental results demonstrate that, when compared to vanilla model checking, our approach achieves a speedup of up to 6.05x, and 2.23x on average.

Related papers

• CASS-RTL: Correctness-Aware Subspace Steering for RTL Generation with LLMs [0.0]
  This work proposes CASS-RTL, a first-of-its-kind framework for discovering and leveraging LLMs' correctness-aware components.<n>We observe 10%-20% improvement in pass@1/5/10 accuracy on VerilogEval and 5% improvement on CVDP.
  arXiv  Detail & Related papers  (2026-06-04T04:02:51Z)
• Opt-Verifier: Unleashing the Power of LLMs for Optimization Modeling via Dual-Side Verification [53.763212981479455]
  We propose a novel framework with Dual-side Verification (Opt-Verifier) from both structure and solution perspectives.<n> Experiments on popular benchmarks demonstrate that our approach achieves over 20% improvement in accuracy.
  arXiv  Detail & Related papers  (2026-05-28T08:09:52Z)
• AHD Agent: Agentic Reinforcement Learning for Automatic Heuristic Design [5.7547035595428255]
  Automatic design (AHD) has emerged as a promising paradigm for solving NP-hard optimization problems.<n>Existing AHD frameworks typically treat large language models (LLMs) as passive generators within fixed contexts.<n>We propose AHD Agent, a novel tool-integrated, multi-turn framework that empowers LLMs to proactively decide whether to generate tools or retrieve targeted evidence.
  arXiv  Detail & Related papers  (2026-05-09T07:36:45Z)
• EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning [4.8941849720433686]
  We introduce EvolveGen, a framework for generating hardware model checking benchmarks.<n>Our approach operates at an algorithmic level of abstraction in which an RL agent learns to construct computation graphs.<n>Our experiments show that EvolveGen efficiently creates a diverse benchmark set in standard formats.
  arXiv  Detail & Related papers  (2026-02-26T04:32:07Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures [8.530369312832084]
  We present FV Debug, an intelligent system that transforms failure traces into actionable insights.<n>Our approach features a novel pipeline: (1) Causal Graph Synthesis that structures failure traces into directed acyclic graphs, (2) Graph Scanner using batched Large Language Model (LLM) analysis with for-and-against prompting to identify suspicious nodes, and (3) Insight Rover leveraging agentic narrative exploration to generate high-level causal explanations.
  arXiv  Detail & Related papers  (2025-09-16T20:22:10Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  We propose a unified Test-Time Compute scaling framework that leverages increased inference-time instead of larger models.<n>Our framework incorporates two complementary strategies: internal TTC and external TTC.<n>We demonstrate our textbf32B model achieves a 46% issue resolution rate, surpassing significantly larger models such as DeepSeek R1 671B and OpenAI o1.
  arXiv  Detail & Related papers  (2025-03-31T07:31:32Z)
• Can Reasoning Models Reason about Hardware? An Agentic HLS Perspective [18.791753740931185]
  OpenAI o3-mini and DeepSeek-R1 use enhanced reasoning through Chain-of-Thought (CoT)<n>This paper investigates whether reasoning LLMs can address challenges in High-Level Synthesis (HLS) design space exploration and optimization.
  arXiv  Detail & Related papers  (2025-03-17T01:21:39Z)
• Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
  Large language models (LLMs) have rapidly advanced and demonstrated impressive capabilities. In-Context Learning (ICL) and. Efficient Fine-Tuning (PEFT) are currently two mainstream methods for augmenting. LLMs to downstream tasks. We propose Reference Trustable Decoding (RTD), a paradigm that allows models to quickly adapt to new tasks without fine-tuning.
  arXiv  Detail & Related papers  (2024-09-30T10:48:20Z)
• AIvril: AI-Driven RTL Generation With Verification In-The-Loop [0.7831852829409273]
  Large Language Models (LLMs) are computational models capable of performing complex natural language processing tasks. This paper introduces AIvril, a framework designed to enhance the accuracy and reliability of RTL-aware LLMs.
  arXiv  Detail & Related papers  (2024-09-03T15:07:11Z)
• InferAligner: Inference-Time Alignment for Harmlessness through Cross-Model Guidance [56.184255657175335]
  We develop textbfInferAligner, a novel inference-time alignment method that utilizes cross-model guidance for harmlessness alignment. Experimental results show that our method can be very effectively applied to domain-specific models in finance, medicine, and mathematics. It significantly diminishes the Attack Success Rate (ASR) of both harmful instructions and jailbreak attacks, while maintaining almost unchanged performance in downstream tasks.
  arXiv  Detail & Related papers  (2024-01-20T10:41:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.