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

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.

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.

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.

Three design choices map directly onto the failures above.

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.

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.

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.

FURTHER READING ON THE WATCHTOWER BRIEF

Sources: case studies and figures from Avestra's internal testing on real designs; product information via avestra.net. AiT is the North American sales representative for Avestra.