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
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 C1 and C2 , 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 → 28 (36.4%)
ES-T1: FIPS-scope cross
6 sampled signals
12 visited
8 retained
16 linked
63 → 16 (74.6%)
ES-T2: FIFO-state cross
5 sampled signals
39 visited
27 retained
41 linked
63 → 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 × cp_key_len × 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 → ral.ctrl_shadowed.mode.set → aes_mode → target and sideload → ral.ctrl_shadowed.sideload → aes_sideload → 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} ∧ aes_keylen inside {AES_256} ∧ 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 , Kt=9 , P=1 , and Kc=19 yield sT=9 and sC=21 , so the target is ConstraintHeavy . It remains in the denominator and is routed to low-beta UCB ( β=0.35 ).
Table 6. End-to-end AES case study.
Setting
λH
λS
λF
λ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.
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.
Infineon Technologies India Private Limited, India · Dr. B R Ambedkar National Institute of Technology Jalandhar, India · Infineon Technologies Dresden AG & Co. KG, Germany
Functional verification dominates integrated circuit (IC) front-end engineering effort, and a single missed bug that escapes to silicon can trigger a costly respin. Recent large language models (LLMs) offer new opportunities to automate this process, yet existing LLM-based approaches generate each component through independent single-turn calls with no shared context, leaving interface mismatches undetected and reported coverage disconnected from specification requirements. To address these challenges, we present GoGoTB, an agentic framework that achieves end-to-end verification closure through three subsystems: an agentic execution control layer, an evolvable knowledge system, and specification-grounded coverage closure. The execution control layer separates deterministic enforcement from LLM reasoning at every tool and stage boundary. The knowledge system dispatches methodology and design-specific expertise on demand. The coverage framework anchors every bin to a named specification behavior so that each residual gap has a diagnosable root cause and a targeted remedy. Tested on 8 register transfer level (RTL) designs without any human intervention, GoGoTB achieves 100% environment generation success and averages 98.4% line, 97.2% branch, 97.0% toggle, and 83.2% functional coverage. No prior work successfully generates a complete verification environment or achieves meaningful coverage on the same benchmarks.
Xin Xin, Jincheng Lou, Junhui Li +11
Tencent · School of Integrated Circuits, Peking University, Beijing · Southwest Jiaotong University +1
Bayesian optimization (BO) is a sample-efficient framework for analog circuit topology search, where evaluating each candidate topology can require costly simulation. However, representation-based BO methods typically treat circuit embeddings as fixed after encoder training. This creates a mismatch between representation learning and optimization: embeddings learned to encode or reconstruct circuit structure are not necessarily organized according to the figure of merit (FoM) being optimized. This paper introduces Test-Time Analog Representation Adaptation for Bayesian Optimization (TTARO), an online deep-kernel BO framework that adapts circuit representations throughout the search process. Starting from pretrained circuit embeddings, TTARO jointly learns a nonlinear feature transformation and a Gaussian-process surrogate using the FoM labels of the circuits evaluated so far. Following each new evaluation, TTARO updates the representation and surrogate before selecting the next candidate. We compare TTARO with conventional Gaussian Process-based BO over fixed embeddings and with Deep Kernel Learning (DKL), which learns the representation only from the initial evaluated designs and keeps it fixed throughout the remainder of the search. By continually incorporating newly observed FoM labels into representation learning, TTARO aligns the search space with the optimization objective as BO progresses. In our experiments, TTARO reduces regret AUC by 15.2% on average relative to BO and by 20.7% relative to DKL across 40 encoder/kernel/acquisition settings, outperforming prior art in most settings with reductions as large as 46.7%.
Fin Amin, Sounak Dutta, Paul D. Franzon
Department of Electrical and Computer Engineering, North Carolina State University, Raleigh, NC, USA