REVIEW 4 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
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 4 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.
Discussion (0). Sign in to comment.