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

Chengjia Liu; Priyadarsi Mishra; David Kebo Houngninou; Michael Quinn; Aakash Tyagi; Jiang Hu

cs.AROct 12, 2026

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

Authors: Chengjia Liu, Priyadarsi Mishra, David Kebo Houngninou, Michael Quinn, Aakash Tyagi, Jiang Hu

Organizations: Department of Electrical and Computer Engineering, Texas A&M University, College Station, Texas, USA · Department of Computer Science and Engineering, Texas A&M University, College Station, Texas, USA

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.

Figures & tables

Figure 1. Overview of the proposed methodology. The workflow is organized into static linkage (A), matched first-pass search (B1), formal triage and routing (B2), and post-cleanup policy-routed BO (B3). The first-pass and post-cleanup loops report simulator-confirmed hits

C_{1}

and

C_{2}

, respectively. Complete unreachability proofs refine the effective denominator without changing the numerator; reachable targets receive a difficulty label and selected policy before post-cleanup BO. A four-stage workflow for non-intrusive last-mile coverage closure. Stage A performs static target-knob linkage using coverage, RTL, and UVM ASTs. Stage B1 runs matched first-pass Bayesian optimization with UVM simulation and coverage-artifact audit. Stage B2 performs formal reachability triage, refines the effective denominator only for complete unreachability proofs, and assigns difficulty labels and policies to retained targets. Stage B3 runs post-cleanup policy-routed Bayesian optimization with simulator-confirmed coverage feedback.

DUT	Initial regression source	CRV runs	Covered	Total bins	Residual targets
AES	Unmodified OpenTitan UVM regression	3,000	227 (83.76%)	271	44
Entropy Source	Unmodified OpenTitan UVM regression	10,000	2075 (91.13%)	2277	202

Table 1. Common initial coverage base. Residual bins define the LMC target set.

Category	AES	Entropy Source
RTL files / RTL LOC	37 / 14,739	18 / 10,511
Testbench files / TB LOC	59 / 7,597	37 / 9,196
Total functional coverage bins	271	2,277
Residual target bins at start	44	202
Total environment knobs	44	63
Verible dependency edges	515	1,653

Table 2. Audited benchmark and measured stage costs. AST-front-end times are approximate; AST/COI times cover the full initial residual target set, formal and model-fit rows report per-query or per-candidate summary statistics, and the total BO-stage row covers the full 20-candidate stage. The total BO-stage wall-clock values include simulation execution and are not full end-to-end workflow runtimes.

DUT	20-simulation branch	Initial covered	New hits	Final raw coverage
AES	Continued CRV	227	1	228/271 (84.13%)
AES	Random over AST/COI-reduced space	227	3	230/271 (84.87%)
AES	BO over AST/COI-reduced space	227	14	241/271 (88.93%)
Entropy Source	Continued CRV	2075	13	2088/2277 (91.70%)
Entropy Source	Random over AST/COI-reduced space	2075	21	2096/2277 (92.05%)
Entropy Source	BO over AST/COI-reduced space	2075	42	2117/2277 (92.97%)

Table 3. Matched search-only baselines under the same initial database and 20-simulation budget. New hits are unique target bins; one simulation may cover multiple bins.

DUT	Sequential stage	New simulator hits	Complete proofs	Inconclusive outcomes	Raw coverage	Effective coverage
AES	First-pass AST/COI + BO	14	–	–	241/271 (88.93%)	–
AES	Complete-proof cleanup	0	2	6	241/271 (88.93%)	241/269 (89.59%)
AES	Post-cleanup group-specific BO	20	2	6	261/271 (96.31%)	261/269 (97.03%)
Entropy Source	First-pass AST/COI + BO	42	–	–	2117/2277 (92.97%)	–
Entropy Source	Complete-proof cleanup	0	10	56	2117/2277 (92.97%)	2117/2267 (93.38%)
Entropy Source	Post-cleanup group-specific BO	93	10	56	2210/2277 (97.06%)	2210/2267 (97.49%)

Table 4. Sequential accounting: only simulator-confirmed first-pass or post-cleanup BO executions add numerator bins, complete-proof cleanup changes only the effective denominator, and difficulty grouping changes only policy selection.

Target	Sampled signals	COI evidence	Interfaces	Linked knobs	Reduction
AES-T1: ECB/AES-256/sideload	3 sampled signals	9 visited	3 retained	28 linked	44 $\rightarrow$ 28 (36.4%)
ES-T1: FIPS-scope cross	6 sampled signals	12 visited	8 retained	16 linked	63 $\rightarrow$ 16 (74.6%)
ES-T2: FIFO-state cross	5 sampled signals	39 visited	27 retained	41 linked	63 $\rightarrow$ 41 (34.9%)

Table 5. Representative target-specific AST/COI linkage funnels. COI is a reduction mechanism, not a coverage metric.

Case-study item	Audited content
Original bin	aes_cov_if::aes_ctrl_cg.cr_mode_key_len.ecb;aes_256;auto[1] , the cp_mode $\times$ cp_key_len $\times$ cp_sideload cross requiring ECB, AES-256, and sideload $=1$ ; initial count 0.
DUT signals	aes_mode , aes_keylen , and aes_sideload , linked to reg2hw.ctrl_shadowed.mode.q , key_len.q , and sideload.q .
COI path	Stored influential interfaces are aes_mode , aes_keylen , and aes_sideload . Representative paths are mode $\rightarrow$ ral.ctrl_shadowed.mode.set $\rightarrow$ aes_mode $\rightarrow$ target and sideload $\rightarrow$ ral.ctrl_shadowed.sideload $\rightarrow$ aes_sideload $\rightarrow$ target, with promoted aliases leading to plusarg/configuration controls.
Linked knobs	Static linkage retained 28 target-linked knobs: 9 temporal and 19 constraint. These category counts enter the difficulty classifier.
Formal property	c_lmc_target uses @(posedge clk_i) disable iff (!rst_ni) with predicate aes_mode inside {AES_ECB} $\land$ aes_keylen inside {AES_256} $\land$ aes_sideload == 1’b1 , bound to the AES top level.
Triage result	Reachable in 2 cycles, with witness depth 2, proof depth 5, solver time 0.48 s, and full Jasper invocation 10.957 s. The classifier inputs $d=2$ , $e=0$ , $M=0$ , $K_{t}=9$ , $P=1$ , and $K_{c}=19$ yield $s_{T}=9$ and $s_{C}=21$ , so the target is ConstraintHeavy . It remains in the denominator and is routed to low-beta UCB ( $\beta=0.35$ ).

Table 6. End-to-end AES case study.

Setting	$\lambda_{H}$	$\lambda_{S}$	$\lambda_{F}$	$\lambda_{C}$	AES hits	ES hits	Purpose
Hit-only	1.0	0	0	0.001	5	27	Value of dense $S/F$ shaping
Default	1.0	0.3	0.2	0.001	20	93	Measured control
High-S	1.0	0.6	0.2	0.001	13	55	Stronger stepping emphasis
No-F	1.0	0.3	0	0.001	21	74	Value of formal alignment

Table 7. Matched objective-weight sensitivity study: 20 simulations per DUT, 28 retained AES targets, and 150 retained Entropy Source targets. Hits are unique newly covered bins, and one simulation may cover multiple bins.

Figure 2. AES endpoint coverage comparison. Panel (a) reports audited raw-coverage endpoints for the matched 20-simulation search branches. Panel (b) reports sequential raw/effective coverage accounting for first-pass BO, complete-proof cleanup, and post-cleanup BO. Solid blue bars use the fixed original denominator, while orange hatched bars use the same numerator with the effective denominator; cleanup changes only the denominator from 271 to 269 and adds no raw hits. No intermediate trajectory is shown. AES endpoint coverage comparison using bar charts. Panel (a) reports raw functional-coverage endpoints for the initial CRV, continued CRV, reduced-random, and first-pass BO branches under the matched 20-simulation search budget. Panel (b) reports raw and effective coverage endpoints for first-pass BO, complete-proof cleanup, and post-cleanup BO. Solid blue bars use the fixed original denominator, orange hatched bars use the same numerator with the effective denominator, and cleanup changes the denominator from 271 to 269 without changing the numerator.

Figure 3. Entropy Source endpoint coverage comparison. Panel (a) reports audited raw-coverage endpoints for the matched 20-simulation search branches. Panel (b) reports sequential raw/effective coverage accounting for first-pass BO, complete-proof cleanup, and post-cleanup BO. Solid blue bars use the fixed original denominator, while orange hatched bars use the same numerator with the effective denominator; cleanup changes only the denominator from 2277 to 2267 and adds no raw hits. No intermediate trajectory is shown. Entropy Source endpoint coverage comparison using bar charts. Panel (a) reports raw functional-coverage endpoints for the initial CRV, continued CRV, reduced-random, and first-pass BO branches under the matched 20-simulation search budget. Panel (b) reports raw and effective coverage endpoints for first-pass BO, complete-proof cleanup, and post-cleanup BO. Solid blue bars use the fixed original denominator, orange hatched bars use the same numerator with the effective denominator, and cleanup changes the denominator from 2277 to 2267 without changing the numerator.

Bayesian Optimization

Bayesian optimization uses probabilistic models and sequential experiments to find strong solutions when evaluating a black-box objective is costly.

See all 240 papers

Agentic AI-based Coverage Closure for Formal Verification
Mar 3, 2026Sivaram Pothireddypalli, Ashish Raman, Deepak Narayan Gadde +1Formal Hardware Verification Formal Verification
Infineon Technologies India Private Limited, India · Dr. B R Ambedkar National Institute of Technology Jalandhar, India · Infineon Technologies Dresden AG & Co. KG, Germany
GoGoTB: Agentic RTL Verification with Specification-Grounded Coverage Closure
Jul 28, 2026Xin Xin, Jincheng Lou, Junhui Li +11Agentic Workflows
Tencent · School of Integrated Circuits, Peking University, Beijing · Southwest Jiaotong University +1
Finding the Needle in a Haystack: Test-Time Analog Circuit Representation Adaptation for Bayesian Optimization
Aug 13, 2026Fin Amin, Sounak Dutta, Paul D. FranzonDeep Kernel Learning Representation Learning
Department of Electrical and Computer Engineering, North Carolina State University, Raleigh, NC, USA

Mar 3, 2026J/K move · Enter open · S save

Agentic AI-based Coverage Closure for Formal Verification

Sivaram Pothireddypalli, Ashish Raman, Deepak Narayan Gadde, Aman Kumar

Infineon Technologies India Private Limited, India · Dr. B R Ambedkar National Institute of Technology Jalandhar, India · Infineon Technologies Dresden AG & Co. KG, Germany

Formal Hardware Verification Formal Verification Agentic Workflows

Open paper AskPDF arXiv

Coverage closure is a critical requirement in Integrated Chip (IC) development process and key metric for verification sign-off. However, traditional exhaustive approaches often fail to achieve full coverage within project timelines. This study presents an agentic AI-driven workflow that utilizes Large Language Model (LLM)-enabled Generative AI (GenAI) to automate coverage analysis for formal verification, identify coverage gaps, and generate the required formal properties. The framework accelerates verification efficiency by systematically addressing coverage holes. Benchmarking open-source and internal designs reveals a measurable increase in coverage metrics, with improvements correlated to the complexity of the design. Comparative analysis validates the effectiveness of this approach. These results highlight the potential of agentic AI-based techniques to improve formal verification productivity and support comprehensive coverage closure.

Abstract

Bayesian Optimization

Explore similar work

Agentic AI-based Coverage Closure for Formal Verification

GoGoTB: Agentic RTL Verification with Specification-Grounded Coverage Closure

Finding the Needle in a Haystack: Test-Time Analog Circuit Representation Adaptation for Bayesian Optimization