Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Assertain: Automated Security Assertion Generation Using Large Language Models

Shams Tarek, Dipayan Saha, Khan Thamid Hasan, Sujan Kumar Saha, Mark Tehranipoor, Farimah Farahmandi

Abstract

The increasing complexity of modern system-on-chip designs amplifies hardware security risks and makes manual security property specification a major bottleneck in formal property verification. This paper presents Assertain, an automated framework that integrates RTL design analysis, Common Weakness Enumeration (CWE) mapping, and threat model intelligence to automatically generate security properties and executable SystemVerilog Assertions. Assertain leverages large language models with a self-reflection refinement mechanism to ensure both syntactic correctness and semantic consistency. Evaluated on 11 representative hardware designs, Assertain outperforms GPT-5 by 61.22%, 59.49%, and 67.92% in correct assertion generation, unique CWE coverage, and architectural flaw detection, respectively. These results demonstrate that Assertain significantly expands vulnerability coverage, improves assertion quality, and reduces manual effort in hardware security verification.

Assertain: Automated Security Assertion Generation Using Large Language Models

Abstract

The increasing complexity of modern system-on-chip designs amplifies hardware security risks and makes manual security property specification a major bottleneck in formal property verification. This paper presents Assertain, an automated framework that integrates RTL design analysis, Common Weakness Enumeration (CWE) mapping, and threat model intelligence to automatically generate security properties and executable SystemVerilog Assertions. Assertain leverages large language models with a self-reflection refinement mechanism to ensure both syntactic correctness and semantic consistency. Evaluated on 11 representative hardware designs, Assertain outperforms GPT-5 by 61.22%, 59.49%, and 67.92% in correct assertion generation, unique CWE coverage, and architectural flaw detection, respectively. These results demonstrate that Assertain significantly expands vulnerability coverage, improves assertion quality, and reduces manual effort in hardware security verification.

Paper Structure

This paper contains 26 sections, 1 equation, 1 figure, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Methodology
  4. Formal Problem Formulation
  5. Phase I: Knowledge Mapping
  6. Structural Alignment ($M_{\text{rtl}}$)
  7. Threat Vector Integration ($M_{\text{threat}}$)
  8. Context Intersection
  9. Phase II: Context-Aware Generation
  10. Prompt Engineering & Rule-Based Generation
  11. Functional Property Analysis
  12. Phase III: Self-Reflection Refinement
  13. Experiments and Results
  14. Experimental Results
  15. Assertion Quantity and Correctness
  16. ...and 11 more sections

Figures (1)

  • Figure 1: The workflow of the proposed Assertain framework. The generative module is queried iteratively ($\times N$), emits a structured table that is serialized as JSONL, and the design context injection provides the full RTL source.