What Makes a Good AI-Generated SystemVerilog Assertion Set?
By Madhulima Tewari, CEO and Founder, VerifAIX
The purpose of coding or generating assertions is to improve design quality: to check design functionality and increase confidence in the correctness of the implementation. At the same time, and equally important, assertions must improve the productivity of the engineers who work with them. A good assertion is not only a verification check, it is also a maintainable engineering artifact. Below are several quality and productivity aspects that distinguish useful AI-generated assertions from noisy ones.
The first requirement is basic but essential: assertions must be syntactically correct and compile cleanly together with the relevant RTL. They should use legal SVA constructs, match the design’s clocks and resets, and avoid references to signals or conditions that are not available in the intended scope.
However, a good assertion is more than a line of code that compiles. It is a meaningful verification artifact that helps expose real design bugs, documents intent, and integrates naturally into the verification environment.
Understandability is part of that. Ideally, each assertion should include a concise English comment explaining what it checks and why it matters, describing the expected behavior, the design intent behind it, and any assumptions involved. Where possible it should also reference the sources it was generated from, such as a specification section, an RTL block, a state transition, or an interface protocol rule, since that traceability is what helps engineers review, trust, and maintain the generated assertions. It should carry a useful SVA error message as well, so that when the assertion fails the verification engineer can triage the issue quickly rather than reverse-engineering its purpose from the code.
The best assertions are derived from design intent: specifications, architectural rules, protocol expectations, micro-architectural assumptions, and the RTL implementation. Assertions extracted only from local RTL structures are often much less valuable. They may simply restate what the code already does, rarely fail, and sometimes become trivially true. Such assertions add noise rather than insight and reduce the ROI of assertion-based verification.
Duplication can be another source of noise. Producing many assertions that are syntactically different but semantically equivalent adds little to verification quality and can make the set harder to review, debug, and maintain. A good AI system should identify overlap and present a compact, meaningful set of checks.
Assertions are only one part of a complete set, working alongside assumptions that constrain the environment to legal behavior and coverage that confirms the interesting scenarios are actually reachable and exercised. Because these three depend on one another, a gap in one weakens the others: assertions with nothing to confirm the scenario was reached can pass without ever seeing the case they were meant to catch, and assertions under the wrong assumptions can pass because the environment has been narrowed until the bug is unreachable. Over-constraint is the more serious of the two, because an assumption that quietly excludes legal behavior removes real checking with no failure to signal that anything is missing. A good set treats constraints as first-class objects that are justified and traceable, not as a convenient way to make properties converge.
AI should also draw on the full expressive power of SVA. Simple one-cycle properties, or invariants, can be very powerful, especially when they express high-level design intent rather than merely reflecting the local structure of the RTL. Other strong assertions may require sequences, implications, temporal windows, local variables, sampled values, stability checks, and protocol-level reasoning. In some cases a powerful assertion may require a small amount of auxiliary modeling code, for example to track history, count events, detect transactions, or encode a derived condition, and a good AI system should know when this is justified and generate it cleanly.
For assertions intended to run in formal, provability is part of quality. A property that cannot converge on a proof within available resources gives an inconclusive result, which is neither a pass nor a fail, and often needs to be decomposed or bounded before it yields a useful answer. Writing properties a formal engine can actually discharge, and knowing when a bounded proof is sufficient and when an unbounded one is required, is as much a part of a good assertion set as the correctness of the underlying check. Assertions generated without regard for how they will be proven tend to produce inconclusive noise that engineers then sort out by hand.
The generated assertion set should also be organized in a way that humans can understand. Instead of producing a large flat list, assertions should be partitioned meaningfully: by interface, protocol phase, FSM behavior, datapath consistency, error handling, reset behavior, ordering rules, or other relevant categories. This helps engineers review the results, decide what to keep, and understand the verification coverage being added.
Assertion quality at the level of the individual property does matter, but it is not enough. The more difficult question is whether the set as a whole covers what the specification requires. A set of well-written, non-vacuous, well-commented assertions can still leave requirements unchecked if nothing connects the set back to the intent it is meant to verify. This is why traceability matters at the level of the set and not only the single assertion. This is what lets an engineer see which requirements have corresponding checks and which do not.
In short, a good AI-generated SVA assertion set is not merely correct code. It is precise, non-trivial, explainable, traceable, maintainable, and organized. The goal is to generate assertions that capture real design intent, increase the probability of finding meaningful bugs, improve confidence in design correctness, and do so with careful attention to the ROI experienced by the users.
At VerifAIX, we take a spec-first approach that grounds generated assertions in design intent rather than in local RTL structure, deriving each assertion from a verification trust layer the team has reviewed and approved, and tracing it back to that source. Because the assertions come from that grounded layer, they carry the intent, the source reference, and the failure context described above, and they are organized for engineers to review rather than delivered as a flat list. The goal is the one this article describes: not more assertions, but assertions that capture real intent, find meaningful bugs, and hold up under the review of the engineers who maintain them.