"AssertLLM : Advancing Hardware Verification with AI"
As a formal verification practitioner, I’m excited to share a research paper which i came across from Zhiyuan Yan and co-author's presented at ASPDAC '25. Their work, AssertLLM, tackles a critical challenge in hardware verification: generating high-quality assertions from design specifications.
🔍 Manual Assertion Generation is a Bottleneck
In formal verification, assertion-based verification (ABV) is a cornerstone for ensuring hardware designs meet their specifications. We rely on SystemVerilog Assertions (SVAs) to define properties that our designs must satisfy. But writing SVAs manually has long been a pain point:
1) Time-Consuming ⌛
2) Error-Prone ⚠️
These hurdles create a bottleneck, delaying verification and increasing the chance of costly errors
💡AssertLLM – AI-Powered Assertion Generation:
Enter AssertLLM, an innovative framework that automates SVA generation by processing entire specification documents—text and waveform diagrams alike. Unlike traditional methods, it uses multiple specialized large language models (LLMs) to extract information and produce high-quality assertions.
Natural Language Analyzer 📝
Takes the textual content of the specification (e.g., descriptions, tables).Extracts structured data for each signal using a unified template:
Name: Signal identifier.
Description: Signal details (e.g., bit-width, functionality, interconnections).
Interconnection Signals: Related signals.
This turns unstructured text into a foundation for assertion generation.
Waveform Analyzer 📊
Processes waveforms
Operates in two steps:
Template Generation: Creates templates to describe signal behaviors.
Description Generation: Produces natural language explanations of those behaviors.
This capability is a game-changer—most tools can’t handle waveforms effectively.
SVA Generator ⚙️
Combines outputs from the analyzers and uses Retrieval Augmented Generation (RAG) with a knowledge base of SVA examples.
Recommended by LinkedIn
Generates three types of SVAs:
Width: Verifies signal bit-widths.
Connectivity: Checks signal propagation.
Function: Ensures functional behavior.
The SVAs are validated with a model checker (e.g., Cadence JasperGold) for syntax correctness, formal property verification (FPV) pass rates, and Cone of Influence (COI) coverage.
📊 Results: A Clear Win Over General-Purpose LLMs
The researchers tested AssertLLM on designs like "I2C," "ECG," and "Pairing," benchmarking it against GPT-4 and GPT-3.5.
For "I2C":
AssertLLM: 65 SVAs with 100% syntax correctness, 86% FPV pass rate, and 93% COI coverage.
GPT-4: 75 SVAs, but only 36% syntactically correct, 11% FPV-passing, and 82% COI coverage.
GPT-3.5: Couldn’t even process the multi-modal specs.
Across All Designs:
AssertLLM averaged 100% syntax correctness, 88% FPV pass rate, and 97% COI coverage.
GPT-4 lagged far behind, averaging just 27% COI coverage.
These results highlight AssertLLM’s precision and ability to handle real-world specifications—something general-purpose LLMs struggle to replicate.
🔗 Check It Out:
#FormalVerification #HardwareDesign #AI #LLM #EDA #Innovation #Research #semiconductor
#HardwareVerification
How does AssertLLM analyze waveform diagrams? Does it vectorize them directly, or does it first convert them via OCR? And how does it handle different formats like VCD, FSDB, or waveform viewers (GTKWave, ModelSim, Vivado)? How was the SVA knowledge base built? Was it trained on ASIC-specific data, or does it rely on general-purpose LLMs? And is there any plan to open-source parts of the project—maybe the trained models or assertion datasets?