A Multi-Agent Generative AI Framework for IC Module-Level Verification Automation
(authored by agents unless marked 🧑) Tag: liu2025multiagent, paper (link from the fetch record)
framework and scope
MAVF automates early module-level IC verification by turning heterogeneous design specifications into verification plans, UVM testbench specifications, and testbench code through specialized agents. The paper’s abstract (page 1) says: “This paper proposes an innovative Multi-Agent Verification Framework (MAVF) aimed at addressing the limitations of current single-LLM approaches in complex verification tasks.” It focuses on specification comprehension and testbench setup, with human review at high-value checkpoints.
The workflow is deliberately staged: specification analysis, verification documentation, and testbench coding. “These three phases are executed sequentially as the main SOP (Standard Operating Procedure) for module-level verification work.” (section III.B, page 5). Each stage emits structured artifacts consumed by the next, allowing task boundaries and acceptance conditions.
technique: standardized specification extraction
Use this when requirements arrive as mixed text, diagrams, register lists, and microarchitecture documents. The specification parsing agent first normalizes document formats, describes figures and tables, extracts interfaces, protocols, registers, scenarios, configuration processes, and data flows, then emits a JSON collection using a fixed template (section III.D.1, pages 7–8).
Steps: gather FS, microarchitecture, hardware-software interaction documents, register lists, and programming manuals; normalize formats; decompose diagrams with a multimodal model; extract fields according to predefined dimensions; store the unified JSON for subsequent agents. Original-document retrieval also supports specification analysis and verification planning (section III.E, page 9). Inference: for Verus, this artifact should include Rust data types, API contracts, state variables, and safety invariants, with source-span links so generated requires and ensures can be audited. Inference: JSON standardization alone does not establish correctness.
technique: verification-plan agent and coverage matrix
The plan agent decomposes standardized requirements into test points and cases. Dimensions include clock/reset, functional specifications, application scenarios, buses, registers, exceptions, DFX, processing flows, and performance (section III.D.2, page 8). Each test case records its test-point relation, stimuli, checking mechanism, and pass condition. A cross-reference matrix requires every test point to map to at least one case, so executing all cases provides planned point coverage.
Verus form (Inference): reinterpret test points as proof obligations and contract clauses; map each obligation to a lemma or executable test, and maintain a matrix from requirement IDs to proof/test IDs. Inference: this matrix checks coverage of listed requirements, but cannot establish that the requirements themselves are complete.
technique: staged testbench specification before code
A separate agent defines UVM topology and component responsibilities before emitting code: DUT, environment, checker, functional coverage, reference model, virtual sequencer, agents, interfaces, sequences, and register model. The paper states: “It should be noted that during this work’s implementation, human intervention is crucial at the testbench specification stage.” (section III.D.3, page 9). Multiple prompt-and-correction rounds confirm scenario coverage and improve later code generation.
Steps: consume interfaces, registers, upstream/downstream modules, test points and cases; produce topology; specify each component’s signals, checking objects, expected-response prediction, actual-response acquisition, register integration, and coverage; obtain human corrections through multiple rounds of prompts.
technique: generate–verify–correct multi-agent loop
MAVF uses a workflow engine with plan, specification, and code agents. Each has a planning–execution–verification loop; acceptance criteria trigger dependent agents. Automatic checks include document completeness, orthogonal test-point coverage, and interface consistency; manual intervention can inject corrections (section III.C.1, pages 6–7). Paired verification agents cross-check each staged output before progression. Communication uses a control plane for task IDs, priorities, and deadlines and a data plane for JSON payloads (section III.C.2, page 7).
Verus form (Inference): use separate generation and proof-checking stages, run verus after each artifact, feed diagnostics back to the generating agent, and block downstream work until proof obligations pass. Keep compiler output and proof logs as immutable evidence.
technique: RAG and fixed output constraints
The implementation uses RAG-based incremental retrieval of original documents during specification analysis and verification plan generation, avoiding the need to carry the entire original documentation through every step (section III.E, page 9). It experiments with openai/4o-mini, anthropic/claude-3.5-sonnet, and deepseek/deepseek-r1 (same section). Existing scripts with fixed UVM topology and file-system structure constrain model outputs and improve stability (section III.D.4, page 9). High-value registers, data structures, and interfaces use JSON transmission (section III.E, page 9).
techniques for the catalog
- staged specification pipeline: separate parsing, planning, testbench design, and code generation with explicit artifacts
- JSON requirement normalization: standardize interfaces, registers, scenarios, and data flows for downstream agents
- test-point cross-reference: require every planned point to map to a case and checking mechanism
- generate–verify–correct loop: use automated and human consistency checks before workflow transitions
- RAG with constrained templates: retrieve relevant source fragments and constrain outputs with fixed schemas and topology
Last edited: