Publikation
Modular End-to-End Pipeline for Formal Property Verification using Large Language Models
Luca Müller; Chandan Jha; Benjamin Arlt; Muhammad Hassan; Rolf Drechsler
In: IEEE Computer Society Annual Symposium on VLSI (ISVLSI). IEEE Computer Society Annual Symposium on VLSI (ISVLSI-2026), July 7-10, 2026.
Zusammenfassung
Formal Property Verification (FPV) makes the verification of industry-scale hardware designs feasible by putting the
focus on desired properties that need to be satisfied. However,
writing System-Verilog Assertions (SVAs) based on textual specifications to model these properties is time-intensive and prone to
errors. This can be attributed to the verbosity and ambiguity of
natural language used to specify system behavior. Large Language
Models (LLMs) have been proposed to mitigate errors, cut costs,
and reduce time-to-market during property generation. While
prior works have shown the potential of LLMs in this regard,
there are several limitations that need to be investigated, e.g., the
consideration of only small design sizes, a lack of incorporation
of formal tools, or a focus on only specific types of properties.
In this work, we mitigate these limitations and introduce a
modular, end-to-end pipeline for FPV using LLMs. The evaluation stage is directly integrated with a formal verification tool,
making use of tool feedback in the loop to improve the quality of
generated assertions. Our pipeline is built to act as a baseline for
future research, allowing easy integration of further processing
steps and refinements. We demonstrate the effectiveness of our
proposed approach on two OpenTitan IP modules, evaluating
both syntactic and semantic quality of LLM-generated assertions
and comparing our results to a zero-shot baseline. Experimental
results show that the assertion pass rate can be improved by
more than 2x and formal coverage can be