REVIEW 13 cited by
(Security) Assertions by Large Language Models
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
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.
Forward citations
Cited by 13 Pith papers
-
FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification
FVRuleLearner retrieves learned operator-level reasoning rules to boost the functional correctness of LLM-generated SystemVerilog assertions by roughly 30 percentage points over simple prompting baselines.
-
SVAgent: AI Agent for Hardware Security Verification Assertion
SVAgent is a prompt-engineering framework that decomposes security requirements into sub-questions to generate SystemVerilog assertions with higher reported accuracy and consistency than direct LLM generation.
-
RealBench: Benchmarking Verilog Generation Models with Real-World IP Designs
RealBench measures LLM Verilog generation on complex open-source IP cores with formal verification, and all tested models score near zero on full system designs.
-
SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine
An LLM-based system combining specification analysis, waveform analysis, and Monte Carlo Tree Self-Refine generates SystemVerilog assertions that outperform AssertLLM and ChIRAAG on I2C and RV-Timer designs.
-
Free and Fair Hardware: A Pathway to Copyright Infringement-Free Verilog Generation using LLMs
A new Verilog dataset with license and copyright filtering, a similarity-based copyright violation benchmark, and a fine-tuned Llama model (FreeV) with a 3% reported violation rate and VerilogEval pass@10 gains.
-
AGON: Automated Design Framework for Customizing Processors from ISA Documents
LLM-generated nano-operator functions allow automated synthesis of customized out-of-order RISC-V processors from ISA documents, with simulated 2.35x average speedups over BOOM.
-
Security Properties for Open-Source Hardware Designs
A new open-source benchmark provides SystemVerilog Assertion properties that detect known security bugs in four popular open-source processor designs.
-
RTL-Breaker: Assessing the Security of LLMs against Backdoor Attacks on HDL Code Generation
RTL-Breaker shows that fine-tuning an LLM on a small fraction of poisoned Verilog samples can make it generate malicious RTL code when a specific trigger appears, while still passing VerilogEval functional checks.
-
Masala-CHAI: A Large-Scale SPICE Netlist Dataset for Analog Circuits by Harnessing AI
Masala-CHAI automatically converts schematic images into SPICE netlists using object detection, line detection, and LLMs, producing a 7,500-example open dataset that boosts analog netlist generation Pass@1 by up to 46...
-
Unleashing GHOST: An LLM-Powered Framework for Automated Hardware Trojan Design
An LLM-powered framework can automatically insert functional, synthesizable hardware Trojans into RTL chip designs, and a state-of-the-art ML detector fails to catch them.
-
Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting
AssertCraft generates SystemVerilog assertions from specification documents using subtask decomposition, fine-tuned GPT-3.5, and iterative compiler-guided repair, reporting 7.3x more correct assertions than a plain pr...
-
BugWhisperer: Fine-Tuning LLMs for SoC Hardware Vulnerability Detection
Fine-tuning open-source LLMs on a GPT-generated database of vulnerable RTL designs raises SoC vulnerability detection accuracy from about 40% to 84.8%.
-
Customizing a Large Language Model for VHDL Design of High-Performance Microprocessors
Extended pretraining on proprietary VHDL code and documents improved a Granite LLM's expert-rated explanations of microprocessor VHDL from 43% to 69%, and instruction tuning pushed the expected rating to 71%.
Discussion (0). Continue with ORCID to comment.