Why a Generic LLM Isn't Enough for Assertions: Three Quiet Failures and How Avestra Catches Them

Written by Ashok Mehta | Nov 9, 2026, 1:35:07 AM

WATCHTOWER BRIEF · VERIFICATION · AI-NATIVE DESIGN

AiT × AVESTRA · A VIEW FROM THE WATCHTOWER

BY ASHOK MEHTA, FOUNDER, AVESTRA

Ashok is building agentic AI software for design verification at Avestra. He holds 22 U.S. patents, is the author of three books on SystemVerilog, and was previously at Intel, TSMC, DEC, Data General and AMCC.

A generic LLM writes SystemVerilog Assertions that look right, compile cleanly and still check the wrong thing. We tested that on real designs, and the failures that matter were the quiet ones.

IN BRIEF

Assertions are slow to write well. Close to a fifth of the verification cycle goes into them, so asking an LLM to write them is tempting.

A one-shot LLM hallucinates. In Avestra's testing, more than 30% of generic LLM assertion output was wrong: invented signals, tautologies, broken syntax or broken semantics.

The dangerous failures are silent. Three real cases below: a signal that does not exist, an assertion broken by a width-promotion rule, and a state register quietly truncated.

The fix is architectural, not a better prompt. Ground every signal in the parsed RTL, gate widths deterministically, and cross-check before anything is final.

Ask the right question of any AI verification tool: not how accurate it is, but what happens when it is wrong, and how you would know.

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, so the temptation is obvious: 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. The three cases below are real. Each came from a capable frontier LLM given a careful prompt, and each looked fine at first read.

What happens when an LLM invents a signal?

We asked an LLM to generate assertions for a DMA controller block, and it checked a signal called dma_axi_arlen. That signal is not in the design.

The RTL implemented a reduced, single-beat AXI interface: no burst support, no awlen or arlen, no awburst or arburst. That is standard for a block that never needs bursts, and the signal appears nowhere in the module, neither in the port list nor 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 is not. 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.

Prompting harder does not fix this, because the model's memory of what AXI usually looks like competes with the RTL in front of it. The fix is architectural: extract the exact port list from source before writing a single property, cite a line number for every signal referenced, and flag anything that cannot be found instead of completing the protocol from memory.

Can an assertion be wrong when the RTL is right?

Yes. We gave the LLM an asynchronous FIFO with Gray-coded pointers and an elaborate prompt. The assertion it wrote failed in simulation, and after debugging, the bug was in the assertion, not the RTL. Here is what it generated:

property p_af_no_overflow_001;
  @(posedge wr_clk) disable iff (!wr_rst_n || !rd_rst_n)
  1'b1 |-> ((wr_ptr_bin - rd_ptr_bin) <= (1 << ADDR_WIDTH));
endproperty
a_af_no_overflow_001: assert property (p_af_no_overflow_001)
  else $error("%m Assertion FAILed: AF_NO_OVERFLOW_001 - write pointer overflow");

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, so it 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, which 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, gets 4,294,967,290, and fails on every wrapped value. The fix forces the subtraction to happen at the pointers' own width before the comparison:

property p_af_no_overflow_001;
  @(posedge wr_clk) disable iff (!wr_rst_n || !rd_rst_n)
  1'b1 |-> (($unsigned(wr_ptr_bin - rd_ptr_bin)) <= (ADDR_WIDTH+1)'(1 << ADDR_WIDTH));
endproperty

The model missed these core semantics even after further prompting. That is the case for agent training, cross-checking and re-evaluation: someone has to catch what the first author cannot see.

Why is a false pass worse than a failure?

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, with exactly one bit high at a time.

IDLE  = 5'b00001
START = 5'b00010
READ  = 5'b00100
WRITE = 5'b01000
ACK   = 5'b10000

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, then 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. Connecting 5 bits to a 3-bit port drops the top two:

IDLE  = 5'b00001 -> 3'b001 = 1
START = 5'b00010 -> 3'b010 = 2
READ  = 5'b00100 -> 3'b100 = 4
WRITE = 5'b01000 -> 3'b000 = 0   // bit 3 dropped
ACK   = 5'b10000 -> 3'b000 = 0   // bit 4 dropped

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.

A crash gets investigated immediately. A false pass gets trusted.

How does Avestra prevent these failures?

Avestra is a 14-agent orchestrated system 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.

The Avestra pipeline
ANALYZE	Spec and RTL analysis, run in parallel.
RECONCILE	An RTL-to-spec inconsistency analysis that surfaces gaps before simulation runs, with suggested fixes to the RTL, the spec or both.
GENERATE	Assertion generation and optimization, re-looped to confirm exhaustiveness, corner cases and correctness.
CROSS-CHECK	Agents check each other's output before anything is considered final.
DELIVER	A cover-driven SVA testbench, verified and ready for silicon.

Three design choices map directly onto the failures above.

GROUNDED, NOT REMEMBERED	Avestra draws on a proprietary retrieval database built from 22 US patents and three SystemVerilog Assertion textbooks, plus a proprietary rule set, 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 and flags anything it cannot find. That is how a signal like `dma_axi_arlen` never reaches the output.
CHECKED BY MACHINE	An LLM's 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 final. If `c_state` is [4:0] in the RTL and [2:0] in the assertion module, that is an automatic hard rejection.
RE-EVALUATED UNTIL IT HOLDS	Subtle SystemVerilog rules, like the width promotion in the FIFO case, 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. Tautologies are filtered out, and every assertion is paired with a cover property.

What should you ask any AI verification tool?

The question is not “how accurate is it?” It is “what happens when it is wrong, and how would I 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 THAT SEPARATE THE TOOLS

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 gives you plausible-looking SVA quickly. On a real design headed to tapeout, what you need is SVA you can trust, so your engineers spend their time on design intent instead of waveform archaeology.

WATCH THE 5-MINUTE WALKTHROUGH

Ashok walks through these cases and how Avestra handles them in a short technical video. Watch it here.

Frequently asked questions

What is a SystemVerilog Assertion (SVA)?

A SystemVerilog Assertion is a formal statement of how a design must behave, checked continuously in simulation or proven with formal tools. Assertions catch protocol violations, illegal states and data corruption close to where they happen, rather than at the output.

Why do LLMs hallucinate when generating assertions?

A general-purpose LLM predicts what usually appears in similar designs. When the RTL in front of it differs from the common pattern, such as a single-beat AXI interface without burst signals, the model can fill the gap from memory instead of reading the source.

What is a false pass in verification?

A false pass is a check that reports success while testing the wrong thing, for example an assertion wired to a truncated signal. It is more dangerous than a failing check because it is trusted rather than investigated.

How is an agentic assertion generator different from prompting an LLM?

An agentic generator runs a pipeline of specialized agents that parse the RTL and spec, generate properties, check widths and signal names deterministically, and cross-check each other before output is final. A single prompt has none of those gates.

How should a team evaluate an AI verification tool?

Run it on your own RTL and ask what happens when it is wrong: whether signals and widths are checked against the parsed source, whether every assertion traces to a requirement, and whether the tool flags what it cannot find.

AiT represents Avestra in North America. If your team is weighing AI-generated assertions, we would be glad to set up a technical session with Ashok on your own RTL. Reach Simon directly at simon@ai-techsales.com.