Assertain: Automated Security Assertion Generation Using Large Language Models

TL;DR

Assertain is an automated framework that uses large language models to generate security assertions for hardware designs, significantly improving correctness and coverage over existing methods.

Contribution

The paper introduces Assertain, a novel LLM-based system that automates security property generation for hardware, integrating design analysis, CWE mapping, and threat intelligence.

Findings

Outperforms GPT-5 in assertion correctness by over 61%

Achieves 59.49% higher CWE coverage

Detects architectural flaws more effectively

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.