Every verification team has lived this moment: a design passes thousands of simulation cycles, then weeks later, under one specific traffic pattern, it silently corrupts data. That is where SystemVerilog Assertions stop being a checkbox and become the thing standing between you and a re-spin.
Writing them well is slow. Nearly 20% of the verification cycle goes to assertion generation, so the temptation is obvious: just prompt an LLM. It can write RTL, write assertions, and explain bugs.
But it is a one-shot tool, and a one-shot tool hallucinates. A generic LLM hallucinates on more than 30% of outputs: invented signals, tautologies, broken syntax or broken semantics.
The three cases below are real. Each one came from a capable LLM given a careful prompt, and each one looked fine at first read.
Case 1: the signal that doesn't exist
We asked an LLM to generate assertions for a DMA controller block, and it checked a signal called dma_axi_arlen that is not in the design.
The RTL implemented a reduced, single-beat AXI interface: no burst support, no awlen/arlen, no awburst/arburst. That is standard for a block that never needs bursts. The signal dma_axi_arlen appears nowhere in the module, not in the port list and not internally.
The model pattern-matched. It saw something that looked like AXI, remembered that AXI4 normally has arlen, and quietly filled the gap with a signal that "should" be there instead of flagging that it isn't.
In verification, a hallucinated signal is not a typo. It is an assertion that fails to elaborate, or worse, one plausible enough to slip through review.
No amount of "prompt harder" fixes this, because the model's memory of what AXI usually looks like competes with the RTL sitting in front of it. The fix is architectural. An agent must extract the exact port list from source before writing a single property, cite a line number for every signal it references, and flag anything it cannot find instead of completing the protocol from memory.
Case 2: the assertion that was wrong, not the RTL
We gave Claude an asynchronous FIFO with Gray-coded pointers and an elaborate prompt, and the assertion it wrote failed in simulation. After debugging, the bug was in the assertion itself, not the RTL.
Here is what it generated:
It looks benign, and a careful reviewer could easily approve it. The root cause is a SystemVerilog rule most engineers never think about.
(1 << ADDR_WIDTH) is an unsized literal expression, which is 32 bits wide. Because it sits on the other side of the <=, the subtraction is promoted to a 32-bit context before it executes. Both 3-bit pointers are zero-extended first, then subtracted, and that destroys the mod-8 wraparound the design relies on.
With wr_ptr_bin = 0 and rd_ptr_bin = 6, the intended result is (0 - 6) mod 8 = 2. The assertion instead computes 0 - 6 in 32-bit unsigned arithmetic and gets 4294967290, which fails the bound on every wrapped value.
The fix forces the subtraction to happen at the pointers' own width before the comparison:
Claude missed these core semantics even after further prompting. That is the case for rigorous agent training, cross-checking and re-evaluation: someone has to catch what the first author cannot see.
Case 3: the helpful decision nobody asked for
Given a one-hot FSM with five states, the LLM sized the state register for a binary encoding and silently dropped the top two bits.
One-hot encoding gives each state its own bit, so five states need five bits, and exactly one bit is high at a time:
The RTL declared the state register as [4:0] c_state. The LLM saw five states and applied the textbook rule for binary encoding: ceil(log2(5)) = 3 bits. It declared the assertion module's state port as [2:0] and wired it up. Nothing in the RTL suggested 3 bits. It was a correct rule applied to the wrong situation, with total confidence.
Many simulators only warn on a width mismatch at a bind connection, so the file compiled and the assertions ran. But connecting 5 bits to a 3-bit port drops the top two bits:
WRITE and ACK, two states that must be distinct, collapse to the same value. The assertions did not fail loudly. They checked the wrong thing and reported success. In our run, debugging showed some of the 5-bit state registers were being zeroed out.
A false pass is more dangerous than a crash. A crash gets investigated immediately, and a false pass gets trusted.
What Avestra does differently
Avestra is a 14-agent orchestrated system purpose-built for tapeout-quality SVA and coverage generation. It is not a single LLM call. It is a phased pipeline in which each agent cross-checks and refines the work of the one before it:
- Spec and RTL analysis, run in parallel.
- An RTL-spec inconsistency analysis that surfaces gaps before simulation ever runs.
- Suggested fixes to the RTL, the spec, or both.
- Assertion generation and optimization. Reloop to confirm exhaustiveness, corner cases, and correctness.
- Cross-checking across agents.
- A cover-driven SVA testbench, verified and silicon-ready.
Three design choices map directly onto the failures above.
Grounded, not remembered. Avestra draws on a proprietary RAG database built from 22 US patents and three SystemVerilog Assertion textbooks, a proprietary Rule Set, and not a generic internet search. Before writing a property, an agent extracts the exact port list from the RTL, cites the source line for every signal it uses, and flags anything it cannot find. That is how a signal like dma_axi_arlen never reaches the output.
Checked by machine, not promised by a model. An LLM promise is only a probability. Avestra parses the RTL and diffs every signal and parameter width in the generated assertion file against the literal declaration before the file is considered final. If c_state is [4:0] in the RTL and [2:0] in the assertion module, that is an automatic hard rejection, not something a smarter prompt is hoped to catch.
Re-evaluated until the semantics hold. Subtle SystemVerilog rules, like the width promotion in Case 2, are exactly what a one-shot generator misses and a cross-checking pipeline catches.
Every Avestra output is traceable to the spec requirement behind it and ships with a confidence score. Avestra is built so that tautologies are filtered out and every assertion is paired with a cover property.
Ask what happens when the tool is wrong
The question to put to any AI verification tool is not "how accurate is it?" It is "what happens when it's wrong, and how would you know?"
An invented signal name is a nuisance you will catch on first read. A confident, quietly wrong engineering decision that compiles, runs and reports success is the failure worth designing against. Three questions separate the two kinds of tool:
- Is every signal, parameter and width checked against the parsed RTL by a deterministic gate, or only by the model's own promise?
- Can every assertion be traced to the spec requirement and the RTL line behind it?
- Does the tool flag what it cannot find, or does it fill the gap from memory?
A generic LLM can give you plausible-looking SVA quickly. Avestra gives you SVA you can trust on a real design headed to tapeout, so your engineers spend their time on design intent instead of waveform archaeology.
The fourteen-agent Avestra Studio pipeline
Learn more at avestra.net.