Saved in:
Bibliographic Details
Main Authors: Tarek, Shams, Saha, Dipayan, Hasan, Khan Thamid, Saha, Sujan Kumar, Tehranipoor, Mark, Farahmandi, Farimah
Format: Preprint
Published: 2026
Subjects:
Online Access:https://arxiv.org/abs/2604.01583
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866911562412851200
author Tarek, Shams
Saha, Dipayan
Hasan, Khan Thamid
Saha, Sujan Kumar
Tehranipoor, Mark
Farahmandi, Farimah
author_facet Tarek, Shams
Saha, Dipayan
Hasan, Khan Thamid
Saha, Sujan Kumar
Tehranipoor, Mark
Farahmandi, Farimah
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2604_01583
institution arXiv
publishDate 2026
record_format arxiv
spellingShingle Assertain: Automated Security Assertion Generation Using Large Language Models
Tarek, Shams
Saha, Dipayan
Hasan, Khan Thamid
Saha, Sujan Kumar
Tehranipoor, Mark
Farahmandi, Farimah
Cryptography and Security
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.
title Assertain: Automated Security Assertion Generation Using Large Language Models
topic Cryptography and Security
url https://arxiv.org/abs/2604.01583