arXiv preprint ·
Formal-Verification-Guided Bayesian Optimization for Non-Intrusive Last-Mile Coverage Closure
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
Abstract
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.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Hardware Architecture
SafeDSE: Joint Exploration of Safety Architecture Patterns, Mapping, and Scheduling for Dataflow Applications With Safety Arguments (Extended Version)
HILO: Enabling Low-power, Dual-Band Communication using Tunnel Diode Oscillators
FORGE: Procedural Weight Generation for Sparse MoE Inference
Where the SRAM Goes: Per-Symbol Attribution of Static Memory in FreeRTOS-C and Embassy-Rust IoT Firmware on a 64 KB RISC-V Microcontroller
LocalTrain: Integer-Only Local Learning for Energy-Efficient CNN Training on Edge FPGAs
Get the few papers worth your time in Hardware Architecture every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.