Chip verification still depends heavily on expert-written correctness specifications. This manual specification step is one of the major bottlenecks for fully automated chip verification.
FM-Agent now extends its specification-generation capability from software to hardware. It can automatically generate correctness specifications for Chisel modules and connect directly with UCAgent, a chip verification agent that consumes specifications to build test infrastructure, generate tests, run simulations, improve coverage, and report bugs.
On the XiangShan Sbuffer module, UCAgent using FM-Agent-generated specifications reaches coverage very close to expert-written specifications: 95.6% code coverage compared with 96.5%, while achieving 100% functional coverage in the reported experiment.
Connecting FM-Agent and UCAgent
UCAgent is designed to automate chip verification once a specification is available. The remaining bottleneck is that specifications are usually written by experts, which is expensive and slow as hardware modules become more diverse and complex.
FM-Agent fills that gap by generating the specification automatically. The resulting workflow connects chip specification generation with chip correctness verification: FM-Agent analyzes Chisel code and generates module specifications, then UCAgent uses those specifications to complete the verification process.
Usage
The chip specification generation feature is available on the chip branch of the FM-Agent repository. Add --hardware when running FM-Agent on a directory containing Chisel code:
uv run python main.py proj_dir --hardware
For a chip module named <module>, FM-Agent writes the generated specification to proj_dir/fm_agent/extracted_functions/<module>_spec.md.
What a Chip Specification Contains
Software functions have clear execution boundaries: a function is called, it runs, and it returns. Software specifications can therefore be expressed with preconditions and postconditions. Hardware modules are different. A chip module runs continuously under a clock, and its outputs depend on inputs, internal registers, and cycle-by-cycle state transitions.
For this reason, FM-Agent adopts the chip specification format used by UCAgent rather than software-style preconditions and postconditions. A chip specification includes port lists, state machines, function groups, function points, checkpoints, and reset handling.
In the example, an 8-bit register has input in, enable signal en, and output out. When en=1, the module updates out to in on the clock edge. When en=0, out keeps its previous-cycle value.
From Software Specifications to Hardware Specifications
FM-Agent originally generated software specifications in a top-down way. It builds a function call graph, starts from top-level functions, and derives both the specification of each function and the expected behavior of its callees. This passes design intent down the call graph.
The same idea transfers naturally to hardware. In software, functions call functions. In hardware, modules instantiate submodules. A software function call graph corresponds to a hardware module instantiation graph.
FM-Agent uses three main steps for chip specification generation:
- Build the module instantiation graph. FM-Agent analyzes Chisel code and identifies how modules instantiate one another.
- Generate specifications and expected specifications. Top-level modules are specified from their Chisel code; submodules are specified using both their own code and expectations propagated from parent modules.
- Generate and validate labels. FM-Agent creates unique labels for function groups, function points, and checkpoints so UCAgent can align specifications, tests, coverage data, and verification reports.
With this workflow, developers only need to provide Chisel code. FM-Agent analyzes the module structure, generates chip specifications, and reduces the manual effort that previously required hardware verification expertise.
Conclusion
FM-Agent extends its software specification generation paradigm to chip verification. By generating specifications that can be consumed by UCAgent, it helps create an end-to-end automated workflow from Chisel code to verification results.