Publikation
Automation of Polynomial Formal Verification using Large Language Models
Luca Müller; Khushboo Qayyum; Nele Hugo; Muhammad Hassan; Rolf Drechsler
In: 44th IEEE VLSI Test Symposium (VTS). IEEE VLSI Test Symposium (VTS-2026), April 27-29, Napa, USA, 2026.
Zusammenfassung
Current advancements in technology have not only
made digital systems ubiquitous, but also made them functionally
more complex. Since they are in charge of various critical tasks,
it is imperative that they are error-free and perform according to
their specifications, requiring extensive testing before fabrication.
Formal verification methods can guarantee that a circuit is
bug-free, but are prone to time and space explosion, making
their adoption challenging. Polynomial Formal Verification (PFV)
aims to make these formal methods viable for practical use by
establishing polynomial time and space complexity bounds on the
verification of hardware designs. However, this requires a lot of
manual effort in the calculation and proof of these bounds.
In this paper, we automate PFV using Large Language Models (LLMs) and aim to reduce the manual work associated with
proof generation. We implement a framework that automatically
calculates polynomial complexity bounds for the verification of
a given circuit. Based on these bounds, an LLM generates an
executable proof for the Z3 theorem prover. We demonstrate
our framework by evaluating multiple LLMs for the quality
and consistency of generated proofs for different types of adder
circuits, making all code and artifacts openly available