Avestra: Agentic AI for SystemVerilog Assertion Generation

Modern ASIC, SoC, CPU, and GPU development depends on verification processes that detect subtle functional defects before tapeout. SystemVerilog Assertions (SVA) are particularly important because they encode temporal design intent: how signals, states, and transactions must behave across clock cycles. Unlike conventional functional coverage, which measures whether selected values or combinations have occurred, assertions verify ordering, timing, protocol, and state-transition requirements. The same properties can support simulation, emulation, hybrid verification, and formal analysis. However, writing, debugging, and integrating production-quality assertions remain specialist activities and reportedly consume approximately 20% of the overall verification cycle.

And the obvious question: why not just point a general-purpose LLM at this? And to be fair — LLMs already can generate RTL, generate assertions, and explain bugs in plain English. That’s genuinely useful.

But here’s the catch: they’re one-shot. They hallucinate on more than thirty percent of outputs — incorrect assertions, tautologies, wrong syntax or semantics, mishandled asynchronous resets, incorrect interpretation of blocking/non-blocking assignments, etc. There’s no traceability, no cross-check against the RTL or the spec. And, critically, it’s neither repeatable nor deterministic — ask the same question twice and get two different answers. An LLM is not a continuous verification system. It’s a one-shot generator. That distinction is the reason Avestra exists.

Avestra addresses this bottleneck through an orchestrated fourteen-agent architecture. Instead of submitting a specification to a general-purpose large language model and accepting a single generated response, Avestra implements a persistent, phased verification workflow. It accepts specifications in formats such as PDF, DOCX, Verilog, and SystemVerilog, together with the associated RTL implementation. Specialized agents analyze these artifacts independently before exchanging structured results. This separation helps expose contradictions that might be missed if specification interpretation, RTL analysis, and assertion generation were performed in a single prompt.

The Specification Agent identifies behavioral requirements, ambiguities, defects, and underspecified conditions. In parallel, the RTL Agent examines implementation structure and detects potential coding or microarchitectural problems. A Spec-to-RTL Inconsistency Agent then reconciles both representations and proposes corrections to either the specification or RTL. An FSM Extraction and Mapping Agent reconstructs finite-state machines and connects implemented states and transitions to their documented intent. Consequently, assertion generation begins from a reconciled behavioral model rather than from potentially inconsistent source material.

The Assertions Agent converts this model into optimized assert and cover properties. The targeted language surface includes parameterized and asynchronous assertions, multiclock properties, sequence antecedents, local variables, subroutine calls, recursive properties, and nested or chained implication operators. These capabilities are significant because syntactically valid SVA can still be semantically ineffective. A property may be vacuously true, may never activate, may encode an incorrect timing relationship, or may constrain correct behavior too aggressively. Avestra therefore applies cross-checking and vacuity-oriented validation before assembling the final assertion suite.

The architecture combines generative models with deterministic components. Its Artifact File Creator, for example, uses rule-based logic to produce assertion modules, bind files, coverage models, and related deliverables. This hybrid design limits generative reasoning to tasks that require semantic interpretation while using predictable software for structured file construction. A central Reflector Agent coordinates workflow stages and human-review checkpoints. Simulation, testbench generation, visualization, coverage analysis, and post-processing provide externally observable feedback that can drive subsequent correction.

Avestra’s generation process is grounded by a proprietary retrieval-augmented generation corpus reportedly containing 22 granted United States patents, three SystemVerilog, assertion, and functional-coverage textbooks, and additional training material. The white paper attributes a sub-1% hallucination rate to this domain-specific grounding and multi-stage checking. In this context, hallucination includes incorrect assertions, tautological properties, and omitted cover points. Because this performance figure is reported by the product’s authors, independent benchmarking would still be necessary to establish its applicability across different designs and verification environments.

A representative target is a FIFO whose full flag asserts one cycle late because of an off-by-one counter defect and inconsistent assignment semantics. Ordinary regressions may miss the precise traffic pattern that activates the failure, allowing silent data overwrite. A temporal property connecting the counter threshold to immediate assertion of the full flag can detect the error when it occurs.

Bottom line: Avestra is positioned as an upstream verification system rather than an assertion-writing assistant. Its principal contribution is not merely generating valid SVA syntax, but integrating specification analysis, RTL inspection, inconsistency resolution, property generation, coverage-driven stimulus, traceability, and validation into one workflow. This architecture aims to transform assertion development from a multiday manual process into a minutes-scale automated pass while retaining the review points required for sign-off-quality engineering.

Also Read:

Tuple Technologies at DAC 2026

Tuple Technologies Develops AI-powered Infrastructure at 2026 DAC

Rethinking ECAD IT Infrastructure: From Fragmentation to an Engineering Platform