The Watchtower Brief | Verification
Raw LLM output gets 30 percent plus of its assertions wrong. A pipeline that reads the spec and the RTL together, and checks its own work, gets that under 1 percent. Here is why the gap exists, what closes it, and where to watch it run on a real design.
| In brief An agentic assertion pipeline reads the specification and the RTL together, flags where they disagree before a single simulation cycle runs, and generates simulation-ready SystemVerilog Assertions and functional coverage. Our client Avestra (Tuple Technologies) reports under 1 percent incorrect assertions from the pipeline, against the 30 percent plus error rate that raw LLM output produces on external benchmarks. Ashok Mehta, author of the reference SVA handbook, demonstrates it live on a real design on Tuesday, September 22, 10:00 to 11:00 AM PDT. Register here. |
Every verification lead has lived this one. The RTL is clean by the standard of its own testbench. Functional coverage is closing. Regressions are green. Then an integration partner, or an architect who finally has time to read the document, points out that the specification says one thing and the design does another. Nobody wrote a bad line of Verilog. The bug lived in the space between two documents that were never put side by side.
SystemVerilog Assertions were invented for exactly this gap. An SVA property is the specification rewritten as something the simulator can check every cycle. When it fails, it names the cycle and the signal. Consider the simplest kind of interface contract, a request that must be acknowledged within three clocks:
property req_ack_within_3; @(posedge clk) disable iff (!rst_n) req |-> ##[1:3] ack; endproperty assert property (req_ack_within_3);
Five lines. Unambiguous. Executable. And yet most designs ship with a thin layer of assertions around a few interfaces and hope constrained-random stimulus finds the rest. The concept was never the problem. The labor was.
Three things keep assertion coverage thin, and none of them is a lack of belief in the method.
It is a specialist skill. Temporal logic, overlapping versus non-overlapping implication, sampling in the preponed region, vacuous passes, local variables inside sequences. Most DV engineers can read SVA. Far fewer can write a complex property correctly the first time, and the people who can are the same people every project is fighting over.
The specification is prose. It lives in a Word document, a Confluence page, or a table with a footnote that changes the meaning of the row above it. Translating prose into properties is an act of interpretation, and interpretation is where the errors enter. Two engineers reading the same paragraph will write two different assertions, and the specification author would recognise neither.
The schedule always moves left. When tapeout is pulled in, assertion writing is the first task cut, because it does not block anything visible. The design still simulates. Coverage numbers still climb. The cost arrives later, as escapes.
The obvious experiment has been run in every verification group by now: paste a section of the spec into a large language model, ask for SystemVerilog Assertions, and see what comes back. The output looks right. It compiles. That is the trap.
Avestra's comparison against external benchmarks puts raw LLM assertion output at more than 30 percent incorrect. The failure modes are quiet ones. A ##1 where the spec means ##2. An overlapping |-> where the protocol requires |=>. A missing disable iff that fires the property through reset. A signal name taken from the spec's naming convention rather than the one actually declared in the RTL. An antecedent that never becomes true, so the property passes vacuously for the life of the project and checks nothing.
A wrong assertion is worse than no assertion. It either fires falsely and consumes debug hours, or it passes silently and manufactures confidence that does not exist. At a 30 percent error rate, every generated property has to be reviewed by exactly the specialist the tool was meant to relieve.
The difference between one prompt and a pipeline is the difference between asking a junior engineer to write assertions from memory and giving a team the spec, the RTL, a compiler, and a review process. Avestra's pipeline splits the work across agents with distinct jobs and a checking loop between them:
| Read both sources | The specification and the RTL are parsed together into one model of signals, interfaces, clocking and timing. Signal names come from the design, not from the prose. |
| Flag disagreements first | Where the spec and the RTL describe different behaviour, the pipeline reports it before any assertion is generated and before simulation starts. This is the spec-to-RTL gap surfaced at RTL freeze, when it is cheap. |
| Generate SVA and coverage | Assertions and functional coverage are produced against the reconciled model, with the clocking, reset and implication semantics taken from the design rather than guessed. |
| Check its own output | Generated properties are compiled and screened for vacuity and consistency. Anything that fails is rejected and regenerated rather than handed to an engineer to find. |
The result Avestra reports is under 1 percent incorrect, and simulation-ready, meaning the properties bind, compile and run in the existing environment without a rewrite pass. That is not a better version of the one-prompt experiment. It is a different category of tool.
Assertions arrive at the start of verification instead of at the end, so the checkers exist on the first day the testbench runs. Specification disagreements surface at RTL freeze, in a review, rather than in an integration partner's bring-up lab. The functional coverage model exists before the first regression, which means coverage closure measures the design against the spec from week one instead of against whatever the team had time to write.
For anyone who delivers or integrates CPU and SoC IP, this matters more than it does for a standalone block. Assertion correctness is part of the delivery standard. The assertions shipped with an IP are how the integrator proves the block behaves as documented, and how the IP vendor proves the integrator used it as documented. A 30 percent error rate in that layer is not a productivity problem; it is a quality-of-delivery problem.
Slide decks about AI in verification are easy to make. A live run on a real design, with the output visible and the audience allowed to ask what happens when the spec is wrong, is not. That is the format of this session.
Ashok Mehta, founder of Avestra, runs the pipeline end to end and takes questions. Ashok wrote SystemVerilog Assertions and Functional Coverage: Guide to Language, Methodology and Applications (Springer), the handbook most SVA practitioners learned from, holds 22 US patents, and spent his career in CPU and SoC design and verification at DEC, Intel, Applied Micro and TSMC. If you have a hard question about vacuity, multi-clock properties, or what the pipeline does with an ambiguous spec, this is the person to ask it.
| Live demonstration and Q&A Assertion-Driven Silicon Success Tuesday, September 22, 2026 | 10:00 to 11:00 AM PDT Presented by Ashok Mehta, Founder, Avestra (Tuple Technologies) Register for the live demo Who should attend: verification leads, DV engineers, IP delivery and quality owners, and CPU and SoC integration teams responsible for assertion correctness. |
A SystemVerilog Assertion is a temporal property, written in the SVA subset of IEEE 1800 SystemVerilog, that states how a design must behave across clock cycles. When simulation or formal analysis violates the property, the assertion fails and points to the exact cycle and signal. It turns a specification requirement into an executable check.
Yes, but raw output from a single prompt is unreliable. On external benchmarks, more than 30 percent of such assertions are incorrect: wrong clock delays, wrong implication operators, missing reset handling, vacuous passes, or signal names that do not exist in the RTL. An agentic pipeline that grounds generation in both the specification and the RTL, and validates its own output, brings that to under 1 percent.
Agentic means the work is split across specialised AI agents with a checking loop, rather than one prompt and one answer. One agent parses the specification, another reads the RTL, one cross-checks the two and flags disagreements, one generates assertions and coverage, and one compiles and validates the output before anything reaches an engineer.
No. SystemVerilog Assertions are the shared language of simulation and formal. Properties from the pipeline can run under simulation, be handed to a formal engine, or both. The pipeline changes how quickly correct properties exist, not which engines consume them.
Ashok Mehta is the founder of Avestra and author of SystemVerilog Assertions and Functional Coverage: Guide to Language, Methodology and Applications (Springer). He holds 22 US patents and has worked in CPU and SoC design and verification at DEC, Intel, Applied Micro and TSMC.
Avestra (Tuple Technologies) is a client of AI Tech Sales. The 30 percent and under 1 percent figures are Avestra's, from its comparison against external benchmarks; the September 22 session is the place to see the methodology behind them and put questions to the author directly. Register here.