Large language models are getting closer to turning specifications into formal properties that can be used to verify an implementation. In practice, that means AIartificial intelligence can now draft candidate assertions from a spec, protocol standard, or even RTL1. resistor-transistor logicSemiconductor device or transistor technology used to control electrical currents and signals.2. register transfer levelRTL is the hardware description layer where design assumptions are often captured.3. Register-Transfer LevelRTL describes the hardware implementation stage targeted by the benchmark. comments, cutting down the most tedious part of writing SystemVerilog Assertions.
The core idea is straightforward: properties describe logical and temporal relationships between signals, and in verification they become assertions. Because these properties are meant to capture intended behavior without embedding implementation details, they can serve as a specification against which RTL1. resistor-transistor logicSemiconductor device or transistor technology used to control electrical currents and signals.2. register transfer levelRTL is the hardware description layer where design assumptions are often captured.3. Register-Transfer LevelRTL describes the hardware implementation stage targeted by the benchmark. can be checked. The problem has long been that SVA is declarative and difficult to write, especially compared with the procedural languages used elsewhere in the flow.
One technical development accelerating this work is the use of knowledge graphs. Instead of relying on an LLM1. local linear models2. Large Language ModelThe model class referenced in the long-context serving demo. to re-extract context from text every time, a KG stores signals, modules, requirements, and ports as nodes, with explicit relationships between them. That structure is meant to ground the model more reliably than ordinary RAG, reducing the risk of invented signal names or misunderstood dependencies.
The article stresses, however, that specifications are rarely complete. In many real projects, the spec is missing details, changes during development, or does not capture all architectural intent, especially at interfaces where bugs often appear. AIartificial intelligence-generated properties therefore tend to be strongest on structural and syntactic coverage, but weaker on the underlying intent and the “why” behind a rule.
That creates a serious verification risk: syntactically valid properties can still be vacuous, overly permissive, or based on a misread requirement, and formal tools may still prove them green. Several experts cited in the piece argue that generated assertions must be reviewed by engineers who understand the design intent, and that spec auditing and change management remain necessary parts of the flow. Human-in-the-loop review is still required before AIartificial intelligence-generated properties can be trusted as verification evidence.