# (Security) Assertions by Large Language Models

arXiv: https://arxiv.org/abs/2306.14027 · HTML: https://mlsanity.com/paper/2306.14027/

## Key facts

- Cited by 32 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 67 references that are in the map.
- First posted on arXiv 24 Jun 2023.

## Builds on (most cited first, 13 of 13)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Megatron-LM: Training Multi-Billion Parameter Language Models Using Model Parallelism](https://mlsanity.com/paper/1909.08053/) (2019)
- [CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis](https://mlsanity.com/paper/2203.13474/) (2022)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [Benchmarking Large Language Models for Automated Verilog RTL Code Generation](https://mlsanity.com/paper/2212.11140/) (2022)
- [DAVE: Deriving Automatically Verilog from English](https://mlsanity.com/paper/2009.01026/) (2020)
- [Fuzzing Hardware Like Software](https://mlsanity.com/paper/2102.02308/) (2021)
- [TheHuzz: Instruction Fuzzing of Processors Using Golden-Reference Models for Finding Software-Exploitable Vulnerabilities](https://mlsanity.com/paper/2201.09941/) (2022)
- [HyPFuzz: Formal-Assisted Processor Fuzzing](https://mlsanity.com/paper/2304.02485/) (2023)
- [The Unpatchable Silicon: A Full Break of the Bitstream Encryption of Xilinx 7-Series FPGAs](https://mlsanity.com/paper/2105.13756/) (2021)
- [Neural Program Repair: Systems, Challenges and Solutions](https://mlsanity.com/paper/2202.10868/) (2022)

## Built on by (most cited first, 30 of 32)

- [Make Every Move Count: LLM-based High-Quality RTL Code Generation Using MCTS](https://mlsanity.com/paper/2402.03289/) (2024)
- [LLM4EDA: Emerging Progress in Large Language Models for Electronic Design Automation](https://mlsanity.com/paper/2401.12224/) (2023)
- [LLMs and the Future of Chip Design: Unveiling Security Risks and Building Trust](https://mlsanity.com/paper/2405.07061/) (2024)
- [Automatically Improving LLM-based Verilog Generation using EDA Tool Feedback](https://mlsanity.com/paper/2411.11856/) (2024)
- [LLM4SecHW: Leveraging Domain Specific Large Language Model for Hardware Debugging](https://mlsanity.com/paper/2401.16448/) (2024)
- [AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation](https://mlsanity.com/paper/2406.18627/) (2024)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [Hardware Phi-1.5B: A Large Language Model Encodes Hardware Domain Specific Knowledge](https://mlsanity.com/paper/2402.01728/) (2024)
- [Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset](https://mlsanity.com/paper/2503.08923/) (2025)
- [Evaluating LLMs for Hardware Design and Test](https://mlsanity.com/paper/2405.02326/) (2024)
- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [ThreatLens: LLM-guided Threat Modeling and Test Plan Generation for Hardware Security Verification](https://mlsanity.com/paper/2505.06821/) (2025)
- [ZeroLeak: Using LLMs for Scalable and Cost Effective Side-Channel Patching](https://mlsanity.com/paper/2308.13062/) (2023)
- [SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models](https://mlsanity.com/paper/2506.20415/) (2025)
- [ChatSVA: Bridging SVA Generation for Hardware Verification via Task-Specific LLMs](https://mlsanity.com/paper/2604.02811/) (2026)
- [Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting](https://mlsanity.com/paper/2411.15442/) (2024)
- [Towards LLM-based Root Cause Analysis of Hardware Design Failures](https://mlsanity.com/paper/2507.06512/) (2025)
- [LLM-aided explanations of EDA synthesis errors](https://mlsanity.com/paper/2404.07235/) (2024)
- [Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification](https://mlsanity.com/paper/2605.06434/) (2026)
- [Overcoming Vision Language Model Challenges in Diagram Understanding: A Proof-of-Concept with XML-Driven Large Language Models Solutions](https://mlsanity.com/paper/2502.04389/) (2025)
- [SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine](https://mlsanity.com/paper/2506.13983/) (2025)
- [QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis](https://mlsanity.com/paper/2603.14239/) (2026)
- [SafeTune: Mitigating Data Poisoning in LLM Fine-Tuning for RTL Code Generation](https://mlsanity.com/paper/2604.27238/) (2026)
- [Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach](https://mlsanity.com/paper/2312.17353/) (2023)
- [GenEDA: Towards Generative Netlist Functional Reasoning via Cross-Modal Circuit Encoder-Decoder Alignment](https://mlsanity.com/paper/2504.09485/) (2025)
- [CUFG: Curriculum Unlearning Guided by the Forgetting Gradient](https://mlsanity.com/paper/2509.14633/) (2025)
- [GUIDE: GenAI Units In Digital Design Education](https://mlsanity.com/paper/2603.17296/) (2026)
- [FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification](https://mlsanity.com/paper/2604.03245/) (2026)
- [LLMs for Secure Hardware Design and Related Problems: Opportunities and Challenges](https://mlsanity.com/paper/2605.10807/) (2026)
- [Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations](https://mlsanity.com/paper/2609.05658/) (2026)

## Abstract (arXiv)

The security of computer systems typically relies on a hardware root of trust. As vulnerabilities in hardware can have severe implications on a system, there is a need for techniques to support security verification activities. Assertion-based verification is a popular verification technique that involves capturing design intent in a set of assertions that can be used in formal verification or testing-based checking. However, writing security-centric assertions is a challenging task. In this work, we investigate the use of emerging large language models (LLMs) for code generation in hardware assertion generation for security, where primarily natural language prompts, such as those one would see as code comments in assertion files, are used to produce SystemVerilog assertions. We focus our attention on a popular LLM and characterize its ability to write assertions out of the box, given varying levels of detail in the prompt. We design an evaluation framework that generates a variety of prompts, and we create a benchmark suite comprising real-world hardware designs and corresponding golden reference assertions that we want to generate with the LLM.
