LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation

TL;DR

LASA is a framework that uses large language models and retrieval-augmented generation to automatically produce security properties and assertions for SoC designs, significantly improving verification efficiency and bug detection.

Contribution

LASA introduces a novel LLM-based approach with retrieval-augmented generation for automatic, non-vacuous security property generation in SoC verification, reducing manual effort and increasing coverage.

Findings

Achieved an average coverage of ~88% in verification tasks.

Successfully identified five unique bugs in OpenTitan SoC.

Demonstrated high effectiveness across multiple open-source SoC designs.

Abstract

Ensuring the security of modern System-on-Chip (SoC) designs poses significant challenges due to increasing complexity and distributed assets across the intellectual property (IP) blocks. Formal property verification (FPV) provides the capability to model and validate design behaviors through security properties with model checkers; however, current practices require significant manual efforts to create such properties, making them time-consuming, costly, and error-prone. The emergence of Large Language Models (LLMs) has showcased remarkable proficiency across diverse domains, including HDL code generation and verification tasks. Current LLM-based techniques often produce vacuous assertions and lack efficient prompt generation, comprehensive verification, and bug detection. This paper presents LASA, a novel framework that leverages LLMs and retrieval-augmented generation (RAG) to produce non-vacuous security properties and SystemVerilog Assertions (SVA) from design specifications and related documentation for bus-based SoC designs. LASA integrates commercial EDA tool for FPV to generate coverage metrics and iteratively refines prompts through a feedback loop to enhance coverage. The effectiveness of LASA is validated through various open-source SoC designs, demonstrating high coverage values with an average of ~88\%, denoting comprehensive verification through efficient generation of security properties and SVAs. LASA also demonstrates bug detection capabilities, identifying five unique bugs in the buggy OpenTitan SoC from Hack@DAC'24 competition.