Can AI‑generated formal verification harnesses really be trusted in RTL verification?
Featured Speaker: Dr Ramesh Krishnamurthy, Postdoctoral Research Associate of University of Edinburgh
Session: Evaluating AI-Generated Formal Verification Harnesses for RTL Using an Open-Source, Non-Vacuity-Aware Flow We present an open-source, reproducible workflow to evaluate AI-generated formal verification harnesses for RTL, focusing on proof soundness rather than property generation alone. In contrast to prior AI-assisted formal approaches centred on proprietary tools or agent orchestration, our method targets harness quality in a Yosys-based flow. We implement automated non-vacuity checks using cover-reachability tests and assumption-ablation runs to expose over-constrained environments and misleading proofs. Evaluated across multiple RTL design classes and SMT solvers, the framework enables controlled, tool-agnostic benchmarking and provides practical guidance on when AI-generated assumptions and assertions yield trustworthy formal results.
3 Key Points
- Open-source, reproducible AI-assisted formal flow.
- Non-vacuity and over-constraint detection built into the flow.
- Controlled benchmarking across designs and solvers.
Verification Futures UK 2026, co‑located with Semiconductors Futures 2026, organised by Tessolve and Alpinum, taking place on Tuesday, 23 June 2026 at the University of Reading.
Verification Futures + Semiconductors Futures 2026 is a one‑day conference, exhibition, and networking event focused on the challenges and breakthroughs in design verification and semiconductor engineering—from DV methodologies and tools to AI‑driven SoC design workflows and emerging chip technologies. It brings together end users and vendors to collaborate on solutions, share insights, and connect with the global verification and semiconductor community.
By co-locating both events on the same campus and day, attendees can move freely between sessions, gain cross-disciplinary insight, and expand their professional network.
More Info