# Formal-Verification-Guided Bayesian Optimization for Non-Intrusive Last-Mile Coverage Closure

arXiv: https://arxiv.org/abs/2610.17449 · HTML: https://mlsanity.com/paper/2610.17449/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 48 references that are in the map.
- First posted on arXiv 12 Oct 2026.

## Builds on (most cited first, 11 of 11)

- [Improved Training of Wasserstein GANs](https://mlsanity.com/paper/1704.00028/) (2017)
- [AutoBench: Automatic Testbench Generation and Evaluation Using LLMs for HDL Design](https://mlsanity.com/paper/2407.03891/) (2024)
- [Conditional GAN for timeseries generation](https://mlsanity.com/paper/2006.16477/) (2020)
- [LLM4DV: Using Large Language Models for Hardware Test Stimuli Generation](https://mlsanity.com/paper/2310.04535/) (2023)
- [Using Neural Networks for Novelty-based Test Selection to Accelerate Functional Coverage Closure](https://mlsanity.com/paper/2207.00445/) (2022)
- [Efficient Stimuli Generation using Reinforcement Learning in Design Verification](https://mlsanity.com/paper/2405.19815/) (2024)
- [Supervised Learning for Coverage-Directed Test Selection in Simulation-Based Verification](https://mlsanity.com/paper/2205.08524/) (2022)
- [Hybrid Intelligent Testing in Simulation-Based Verification](https://mlsanity.com/paper/2205.09552/) (2022)
- [Detecting Stimuli with Novel Temporal Patterns to Accelerate Functional Coverage Closure](https://mlsanity.com/paper/2407.02510/) (2024)
- [Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification](https://mlsanity.com/paper/2501.01534/) (2025)
- [FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification](https://mlsanity.com/paper/2604.03245/) (2026)

## Abstract (arXiv)

Last-mile functional coverage closure for modern chip designs remains costly because a mature UVM environment exposes many controls while direct hits on the remaining bins are sparse. We present a non-intrusive workflow that closes pre-defined bins in an existing, human-authored functional coverage model; it does not synthesize verification objectives from the design specification. The workflow first uses abstract-syntax-tree (AST) parsing and cone-of-influence (COI) tracing to map each residual target to existing testbench knobs. Under a matched 20-simulation budget, Bayesian optimization (BO) is compared with continued constrained-random verification (CRV) and random search over the same AST/COI-reduced space. Formal reachability then removes only targets supported by complete unreachability proofs, after which retained targets are grouped by formal difficulty and processed by group-specific BO under a second matched 20-simulation budget. Cleanup and grouping never add numerator bins; only simulator coverage artifacts do. On OpenTitan AES, first-pass reduced-space BO reaches 241/271 bins; formal cleanup removes two denominator bins; the integrated post-cleanup stage - difficulty grouping, policy routing, and group-specific BO - adds 20 simulator-confirmed hits, yielding 261/271 raw coverage (96.31%) and 261/269 effective coverage (97.03%). On Entropy Source, first-pass reduced-space BO reaches 2117/2277 bins; formal cleanup removes ten denominator bins; the integrated post-cleanup stage - difficulty grouping, policy routing, and group-specific BO - adds 93 simulator-confirmed hits, yielding 2210/2277 raw coverage (97.06%) and 2210/2267 effective coverage (97.49%). These results characterize the integrated diagnosis-and-search workflow; the present evaluation does not isolate the causal contributions of difficulty classification, policy routing, and post-cleanup BO.