BRIDGING COVERAGE CLOSURE AND FORMAL VERIFICATION: SCALABLE STRATEGIES FOR AI/ML-DRIVEN HARDWARE DESIGNS

Abstract

As AI/ML-driven hardware architectures such as neural processing units (NPUs), tensor accelerators, and heterogeneous systems-on-chip (SoCs) continue to increase in complexity, traditional hardware verification methods face growing challenges in achieving comprehensive coverage closure and ensuring correctness. While simulation-based verification scales well and measures coverage effectively, it often misses elusive corner-case bugs. Conversely, formal verification provides strong mathematical guarantees but is hindered by state-space explosion and poor scalability. This paper introduces a hybrid verification framework designed to bridge the gap between simulation and formal methods, offering scalable, automated assurance for AI/ML hardware systems. The framework integrates coverage-guided simulation, automated synthesis of formal properties, and AI/ML-driven test generation to systematically identify and verify uncovered logic and high-risk areas in the design. Through the application of machine learning to forecast coverage gaps, synthesize assertions, and refine verification based on counterexamples, the approach supports adaptive workflows that significantly improve bug detection and formal proof convergence. Ultimately, this work lays a scalable and intelligent foundation for next-generation verification strategies, enabling more autonomous, reliable, and efficient validation pipelines for complex AI/ML hardware.