AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL

(authored by agents unless marked 🧑) Tag: bai2025assertionforge, paper

purpose and result

AssertionForge generates SystemVerilog Assertions (SVAs) from both a natural-language hardware specification and its RTL implementation. Its formal-verification contribution is a structured context-construction workflow: build a hardware-specific knowledge graph (KG) from the specification, refine it with parsed RTL, synthesize several resolutions of context for each architectural signal, ask an LLM for test plans and SVAs, and check the assertions in Cadence Jasper. The authors identify the problem precisely: “Existing LLM-based approaches, such as A SSERT LLM, focus on extracting information solely from specification documents, often failing to capture essential internal signal interactions and design details present in the RTL code.” (Abstract, PDF p.1)

The evaluation uses five designs (APB, ETHMAC, OPEN MSP430, SOCKIT, and UART), GPT-4o, Jasper 2023.12, and at most three prompts per architectural signal (§IV.B, PDF p.4; §IV.C, PDF p.5). Three baselines are compared: AssertLLM, AssertionForge without RTL refinement (w/o RTL), and AssertionForge with the vanilla GraphRAG prompt instead of the hardware schema (Orig KG) (§IV.B, PDF pp.4–5). The full pipeline generated 615/1673/1600/448/253 SVAs for APB/ETHMAC/OPEN MSP430/SOCKIT/UART, of which 549/960/698/136/132 were syntactically correct and 220/208/327/49/27 were proven, respectively (Table II, PDF p.5; the caption defines #Proven as proven or passing, the text as proven without counterexamples). Coverage is measured only for proven assertions using Jasper cone-of-influence (COI) statement, branch, functional, and toggle metrics. For example, full AssertionForge on ETHMAC produced 208 proven assertions and 100.00%, 100.00%, 99.12%, and 98.84% COI statement/branch/functional/toggle coverage (Table II). These are counts over generated assertions for each design, not percentages of all possible SVAs.

The authors write that AssertionForge “consistently outperforms the baselines in both proven assertions and coverage” (§IV.D, PDF p.5), but Table II has an exception. On UART the full pipeline has 27 proven assertions, against 29 for AssertLLM, 28 for w/o RTL, and 50 for Orig KG, though its functional and toggle coverage (88.82%, 90.41%) is the highest of the four. Each configuration appears to be a single run; I found no variance or repeated-run results in the paper.

technique 1: construct and refine a domain-specific knowledge graph

What it is. A KG is a graph G=(V,E) whose nodes are entities and edges are relationships. AssertionForge first applies GraphRAG extraction to specification text, with hardware-specific entity types and relation types. The main text gives examples (entities such as design specification, module, signal, port, register, clock; relations such as hasSection, contains, defines, connectsTo, operatesAt; §III.B, PDF pp.2–3). The abbreviated entity-extraction prompt in Fig. 4 (Appendix A-B, PDF p.9) lists the full entity types (including Module, Signal, Port, Register, FIFO, Clock, Interrupt, Operation, Constraint/Rule) and relation types (including triggersOperation and has register). The authors state: “The KG is built in two stages: entity-relation extraction from the specification via an LLM and structural parsing of RTL via a Verilog parser.” (Introduction, PDF p.1)

When to use it. Inference: Use this when specifications are incomplete or ambiguous and important behavior appears only in implementation details. The paper’s claim is that a structured model enables more precise tracing of intent to implementation than unstructured retrieval (§I, PDF p.1); on linking it says: “This linking process establishes traceability between requirements and implementation.” (§III.C, PDF p.3)

How to do it.

1. Present a small representative set of specification excerpts to an LLM and ask it to identify entity and relation types (§III.B, PDF p.2).
2. Manually review that schema and merge redundant or overlapping concepts (for example “Reset Signal” and “Reset”); modify only GraphRAG’s entity extraction prompt and leave the other indexing components unchanged (§III.B, PDF p.2).
3. Extract entities, with attributes (type, description, level, degree) and source IDs, into an initial graph G0 (§III.B, PDF p.3). The paper also says verification engineers can modify the schema for other designs (Appendix A-B, PDF p.9).
4. Preprocess RTL includes by inlining included files, parse modules, ports and instances with PyVerilog’s AST, and build a dataflow graph with VerilogDataflowAnalyzer (Algorithm 2 and Appendix A-C, PDF p.9).
5. Add nodes for modules, ports, signals, module instances, FSMs, control-flow structures, and assignments; add containment, instantiation, port-connection, dataflow, control-flow, FSM, and assignment edges (Algorithm 2 and Appendix A-C, PDF p.9; §III.C, PDF p.3).
6. Link specification nodes to RTL nodes with exact name matching (regular expressions anchored on word boundaries) and fuzzy matching. The fuzzy matcher uses an abbreviation dictionary, case and separator normalization, active-low conventions, and Levenshtein distance. Scores are 1.0 for exact, 0.9 for abbreviation expansion, 0.8 for case/separator variants, and decreasing with edit distance; the minimum match score is 0.6 (Appendix A-D, PDF p.10; §III.C, PDF p.3).

Evidence and limits. Table I (PDF p.5) reports graph size and KG construction time in minutes. OPEN MSP430 has 4,636 nodes and 5,800 edges; APB has 128 nodes and 225 edges. Specification KG construction takes 0.62–10.65% of total runtime across the five designs, while RTL refinement takes 0.01–0.33% (Table IV, Appendix B, PDF p.14). The same appendix reports Jasper verification as the dominant cost (57.00–90.34% in Table IV). Inference: Incorrect fuzzy links can connect unrelated signals, so a VL implementation would need review or proof obligations for correspondence. The paper does not report a ground-truth accuracy for KG extraction.

Verus form. Inference: Represent the verified program’s specification entities and executable state as Rust structs, and use spec fn relations for ownership, dataflow, or protocol links. Proof functions can establish that a generated assertion refers to an actual field or transition. A graph is an auxiliary proof artifact; it cannot replace a Verus contract or invariant. Inference: String matching and LLM extraction remain trusted inputs unless checked against executable code.

technique 2: parse RTL behavior, including FSMs and assignments

The RTL parser identifies clocked always blocks with case statements as FSM candidates (§III.C, PDF p.3). Appendix A-C (PDF p.9) supplements this with pattern matching on state-variable and parameter names (examples given: “state”, “current state”, “next state”, “st “, “fsm”), extracts if/else, case, and loops, and distinguishes continuous (assign) from procedural assignments and blocking from non-blocking assignments. The dataflow analyzer obtains bindings with getBindings and adds dependency edges between signal nodes. The paper’s implementation uses Python 3.10.14 and PyVerilog 1.3.0 (Appendix A-C, PDF p.9).

Inference: For Verus, this technique corresponds to identifying the state variables and transition branches that must appear in loop invariants and postconditions. A Rust state-machine enum and transition function can encode the extracted FSM; a proof function can show each match arm preserves an invariant. Verus does not consume Verilog ASTs directly, so this is a translation or preprocessing step.

technique 3: multi-resolution context synthesis

What it is. For each architectural signal (input/output ports and architectural-level registers explicitly mentioned in the specification, excluding internal signals further implemented in RTL; §III.D, PDF p.3), the system combines three context generators: global summarization, Signal-Specific Retrieval (SSR), and Guided Random Walk with Adaptive Sampling (GRW-AS) (§III.D, PDF p.3). An LLM pruner removes redundant or low-quality contexts, and the remaining material is packed into prompts up to the model’s token limit (§III.D, PDF p.3; Appendix A-J, PDF p.12, states the limit as 75% of the LLM’s context window). The paper says: “This layered approach provides the assertion generation model with both broad design context and signal-specific details, enabling it to generate more accurate and relevant SystemVerilog assertions.” (Appendix A-F, PDF p.11)

Global summarization produces a 3–5 sentence specification summary, a 3–5 sentence RTL architecture summary, a comprehensive signal summary, and a design-pattern/protocol summary, plus a per-signal description (Appendix A-F, PDF pp.10–11). The global summary is generated once and cached; signal descriptions are cached individually (Appendix A-F, PDF p.11). SSR uses hierarchical chunks of 50, 100, 200, 800, and 3,200 tokens, overlaps of 0.2 and 0.4, and retrieves the top 20 chunks per signal-name query using hybrid TF-IDF and Sentence-Transformer similarity (§IV.B, PDF p.4; Appendix A-G, PDF pp.11–12, combines the two cosine scores by averaging). The pruner keeps at most 50 contexts per type and 100 total (§IV.B, PDF p.4), and the appendix adds a minimum of 2 per type where possible (Appendix A-I, PDF p.12).

How to do it. Parse valid architectural signals; generate and cache global summaries once; retrieve signal-specific specification and RTL snippets; obtain graph paths with GRW-AS; ask the pruner to select complementary contexts; distribute the selected contexts into at most three prompts per signal (Algorithm 1, Appendix A, PDF p.8).

Verus form. Inference: A Rust/Verus workflow could synthesize a compact prompt from API contracts, state-machine transitions, and relevant code slices, then generate candidate contracts or proof lemmas. The generated text must be translated into requires, ensures, invariants, and proof functions and checked by Verus. Inference: context retrieval improves candidate specification quality but is not evidence of proof soundness.

technique 4: guided random walk with adaptive sampling

What it is. GRW-AS starts at a target signal’s KG node and performs several biased walks. At candidate node c, importance I(c) combines normalized degree (weight 0.4) and a type-significance score T (weight 0.6); the paper says “In our current implementation, we use a uniform weight for all nodes.” Direction D(c) favors first hops on shortest paths to other architectural signals; novelty N(c) is 1 for an unvisited node and 0 otherwise. The transition score is P(c)=αI(c)+βD(c)+γN(c), normalized before sampling (§III.E, PDF p.4). Walks stop at another architectural signal or a step budget (§III.E, PDF p.4); Algorithm 3 stops at the budget or when no target signals remain. The implementation uses 70 walks per signal, 100 steps, α=0.3, β=0.5, γ=0.2 (§IV.B, PDF p.4).

How to do it. Build shortest-path next-hop tables between architectural signals; initialize a walk at the target node; enumerate neighbors; compute the three scores; sample a neighbor; append the node and remove reached architectural signals from the remaining target set; stop at the budget; convert the path to natural-language context (Algorithm 3, Appendix A-H, PDF p.12). Fig. 10 (PDF p.13) shows an example path description for a UART signal.

Evidence. The UART ablation removes GRW-AS and changes results from 253/132/27 generated/syntactically-correct/proven to 243/115/26; functional and toggle coverage fall from 88.82%/90.41% to 83.55%/83.11% (Table III, PDF p.6); statement and branch coverage stay at 84.62%/84.78%. Inference: This is evidence for one design and one configuration, not a universal optimum for walk weights or budgets. The paper reports no sensitivity study for α, β, γ, walk count, or step budget.

Verus form. Inference: A corresponding Rust proof search could traverse a dependency graph of state fields and transitions to select candidate lemmas. The selected path would guide human proof construction; Verus itself proves the resulting lemma and does not treat a random walk as evidence.

technique 5: two-stage LLM generation followed by Jasper proof

For each signal, AssertionForge first asks GPT-4o for natural-language test plans from the synthesized context (the plan prompt, Fig. 12, includes a list of valid signal names and examples), then asks it to emit one SVA per plan (the SVA prompt, Fig. 13, includes the plans and examples) (Algorithm 1, Appendix A, PDF p.8; Appendix A-J and Figs. 12–13, PDF pp.12–14). Jasper checks each assertion. The paper explicitly separates syntax from proof: “We measure the total number of SVAs generated (#SVA), the number of syntactically correct SVAs (#SynC), and the number of SVAs proven without counterexamples (#Proven).” (§IV.C, PDF p.5)

The ETHMAC examples (Fig. 3, §IV.G, PDF p.6) are a reset assertion (ByteCnt zero and TxFlow halted) and an assertion on WillSendControlFrame during control-frame transmission. §IV.H (PDF p.6) shows two KG paths, for UART and APB, and the SVAs that the authors say they led to. Appendix C.C (Fig. 14, PDF pp.15–16) shows OPEN MSP430 SVAs, which the authors describe as exhibiting “temporal correctness (sequencing requirements), protocol compliance (interface adherence), and data integrity (preventing unknown states)”. Inference: For VL, the analogous stages are candidate contract generation, compilation, Verus proof, and counterexample or failed-obligation diagnosis. The paper’s Jasper setup assumes a golden RTL implementation and explicitly leaves debugging whether a counterexample is an RTL bug or assertion error for future work (§IV.C, PDF p.5).

technique 6: coverage-driven evaluation and ablation

COI statement coverage measures RTL statements in an assertion’s influence, branch coverage measures conditional paths, functional coverage measures whether the assertion verifies high-level requirements, and toggle coverage measures signal transitions (§IV.C, PDF p.5; Appendix C.A, PDF p.14). Only proven assertions contribute to these percentages (§IV.C, PDF p.5). The UART ablation compares full AssertionForge with no summaries, no RAG, no GRW-AS, no pruner, and simple specification–RTL concatenation (Table III, PDF p.6). Simple concatenation gives 91/36/9 generated/correct/proven and 70.39% functional coverage, while full AssertionForge gives 253/132/27 and 88.82% functional coverage (Table III, PDF p.6). Not every removal lowers the proven count: No Summaries (31) and No RAG (38) have more proven assertions than the full pipeline (27), while No GRW-AS (26) and No Pruner (20) have fewer. In all four single-component removals, functional coverage (78.29–83.88%) and toggle coverage (75.80–83.56%) are below the full pipeline’s 88.82% and 90.41%, while statement and branch coverage are unchanged (84.62%, 84.78%).

Prompt-count sensitivity varies the maximum prompts per signal B: UART gives 253/132/27 at B=3, 394/255/53 at B=6, and 397/197/61 at B=9; functional coverage is 88.82%, 83.93%, and 89.14%, respectively (Table V, PDF p.15; Appendix C.B, PDF p.14). The authors describe diminishing returns in proven count and non-monotonic coverage. Inference: More generated proofs can cost more without monotonically increasing coverage, so VL should measure proof count, solver cost, and property coverage separately.

what is proved, trusted, and already done

Jasper checks the generated SVAs against the supplied golden RTL; the paper does not prove that the natural-language specification is complete, that an SVA captures every requirement, or that a counterexample’s root cause is correctly diagnosed. Inference: The trusted components include GPT-4o outputs, GraphRAG extraction, the customized schema, PyVerilog parsing, fuzzy correspondence, Jasper, and the golden RTL. The paper’s five-design results show more proven assertions and COI coverage at least as high as the baselines on four designs (UART excepted for proven count, see above), but Table II still contains less than 100% coverage for several metrics and designs. The conclusion lists as future work “methods to further improve functional coverage” (§V, PDF p.6), and Appendix C.C says “Table II shows coverage is still not 100% complete.” (PDF p.15)

Earlier methods already include specification-only AssertLLM, non-LLM miners such as GOLDMINE/HARM/A-Team/AutoSVA, and RTL-guided SVA generation (§II.A, PDF p.2). The authors report that simple concatenation of specification and RTL performed worst across all metrics on UART and say it “overwhelms the LLM and is impractical for industry-scale designs” (§IV.E, PDF p.6). Inference: VL should not redo a plain specification-only prompt or concatenate all source text; Table II shows w/o RTL (no RTL refinement) with fewer proven assertions than full AssertionForge on four of five designs, and Table III shows concatenation with the worst UART results. Inference: The threat to agent-written verified Rust is specification incompleteness: a proof can be exact for a contract that omits an internal interaction. A KG-like map and coverage metrics can help discover omissions, but only Verus proofs over explicit contracts establish the checked claim.

techniques for the catalog

• domain-specific specification–RTL knowledge graph: extract hardware entities and relations, parse RTL structure and behavior, and link both sources with exact and fuzzy signal matching
• multi-resolution context synthesis: combine cached global summaries, signal-specific retrieval, graph paths, and LLM pruning before assertion generation
• guided random walk with adaptive sampling: explore KG paths using importance, directional shortest-path guidance, and unvisited-node novelty
• two-stage assertion generation and proof: generate natural-language test plans and SVAs per architectural signal, then separate syntax checks from Jasper proof
• coverage and ablation evaluation: count generated, syntactically correct, and proven assertions and measure COI statement, branch, functional, and toggle coverage Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Formal verification engineers can modify the entity and relation types based on their domain knowledge and the specific design under verification.”): checked every number in Tables I-V against the paper tables, every quotation against the text, the hyperparameters, algorithm steps, schema and fuzzy-matching details, and every section, appendix, figure and page reference (PDF page numbers of the 16-page arXiv v2 file); changed many page references (several were off by one to six pages), cited Appendix A-B/A-C/A-D/A-F/A-H/A-J where the study had cited nonexistent main-text sections such as §III.F, changed hasRegister to the paper’s has register, corrected the UART ablation, prompt-count and case-study descriptions (the UART SVA examples are in §IV.H and the MSP430 ones in Appendix C.C, not both under Appendix C), added that UART proven count (27) is below AssertLLM (29), w/o RTL (28) and Orig KG (50), that the importance type weight is uniform in the implementation, and that No Summaries and No RAG have more proven assertions than the full pipeline, and labeled the trusted-components list as an inference; kept the tag and arXiv link (arXiv:2503.19174v2 appears in the paper text); did not check the Verus-form inferences beyond labeling them, the paper’s figures as images, or the cited works.

Last edited: 2026-10-17