Why are simulation-only verification flows failing modern chips?
Introduction
Modern chip designs are pushing the boundaries of complexity, driven by demands in artificial intelligence, automotive, high-performance computing, and communications. The costs of advanced technology nodes such as 3nm FinFET mean that errors can cost hundreds of millions of dollars, or even more when delayed product releases are factored in. Verification remains the bottleneck in the development process, consuming up to 80% of design cost and time [1]. Verification efficiency thus has the biggest impact on cost and time-to-market, while the effectiveness of that verification impacts errors in final silicon. Traditional simulation-only flows, while long-established, are struggling to keep pace with this complexity.
Simulation relies on constrained random test benches, which can leave holes in coverage, especially for edge cases. Logic or functional flaws remain the leading cause of respins in modern designs, as highlighted by the Wilson Research Group report [2]. The report also highlights the growth in formal verification, providing rigour and the potential for both completeness and elimination of respins.
The Structural Limits of Simulation
Simulation’s core weakness is its reliance on specific test vectors to explore the design space. As design complexity increases, the number of possible states and interactions grows exponentially, making exhaustive simulation impossible. Based on data from [1], Figure 1 Illustrates a suggested exponential relationship between verification and design complexity.
How Formal Verification Works Compared to Simulation
Simulation only often means incomplete coverage, especially for corner cases, and “bug escapes”. The effort in building, validating, and maintaining complex testbenches can be prohibitive. Simulation failures often occur later, leading to longer debug and fix cycles, increased costs and tapeout delays.
Public reports of chip errors are, unsurprisingly, rare. However, errata notices offer examples such as “a Global Timer sending two interrupts for the same event” or, more critically, “Deadlock on a sequence of cancelled Advanced-SIMD or VFP stores” from ARM [3]. Intel’s bug affecting the Sandy Bridge processor BER (bit-error rate) was discovered post-silicon after both Intel and its OEMs signed it off [4]. The infamous FDIV bug of the 1990s cautions against simulation-only flows and triggered Intel’s wider adoption of formal verification [5].
How Formal Verification Bridges the Gap
Formal verification complements simulation by mathematically “proving” that a design meets its specification across all possible states. This approach eliminates reliance on testbenches and stimulus generation, offering complete and exhaustive coverage by exploring the full design state spaces.
To illustrate this, consider the example in Figure 3. The example shows two blocks with “Block A” requesting permission to send (given via the “grant” signal) to send data. The data would be sent via a “data” bus controlled by a “valid” signal (not shown) once the permission is given.
To explain the SVA code in Figure 3:
- SVA1 = “(request && !grant) |-> ##1 request” says that if a request is made but permission is not granted, then the request must continue in the future until permission is given
- Block A must guarantee this
- Block B can assume this (once the guarantee from Block A is proven) assume((request && !grant) |-> ##1 request)
- SVA 2 = ”request |-> s_eventually grant” sets up the obligation for Block B to guarantee that permission will eventually be granted
We can now use formal verification to prove SVA2 under the assumption of SVA1. Please note that the proof will handle the infinite time possibly required for permission, implied by the s_eventually operator. This proves that permission is “eventually” granted, thus avoiding a livelock. This could never be done through simulation alone.
The cover statement can be used to ensure that the space searched by the formal verification includes states where the preconditions of the properties occur. For example:
- Cover1 = “cover (request && !grant)”
The verification environment and runtimes for the above example are typically much lower than those for the simulation-based alternative. It can also be easily extended to prove that valid data is eventually sent once permission is granted.
Thus, formal verification can save cost and time as the verification environments are easier to build and reuse. These benefits enable earlier bug detection, especially if used by designers (with the usual caution of maintaining verification independence).
LUBIS EDA’s formal verification solutions can also automate the generation of assertions, help with checkers and functional coverage, and apply Abstractions. Additionally, LUBIS integrates with continuous integration tools to access regression history, enhancing reproducibility and reports for easier adoption
Real-world examples
LUBIS EDA’s formal verification solution has uncovered critical bugs in AXI protocol blocks, caches, and RISC-V cores that simulation-only flows have missed. For example, detecting six AXI protocol violations, including handshake and 4 KB boundary violations, which required a major redesign [6]. LUBIS EDA identified a scenario where uncached requests were dropped under specific backpressure and missed in simulation [6][7]. Initial verification of the RISC-V core uncovered over 50 bugs, including incorrect exception handling and instruction execution [6]. The highlighted references demonstrate how LUBIS EDA automation enables bug detection, accelerates proof convergence, and reduces verification time and cost.
Conclusion
Simulation-only verification flows are no longer sufficient. Complex chip designs also require formal verification to meet today’s safety and reliability demands. LUBIS EDA’s automation technologies offer the efficiency, scalability, and completeness required to ensure silicon confidence.
Explore LUBIS automation for formal verification to future-proof your chip development and gain a competitive edge.
As chip complexity increases, simulation-only flows fall short of guaranteeing functional safety. Formal verification, with exhaustive analysis and earlier bug detection, provides the coverage and confidence needed for successful silicon implementation.
References:
[1] Q. Shao and J. Yan, “Formal verification in chip verification and study on its application practice,” in Proc. SPIE 12635, AMNA 2023, SPIE-Intl Soc Optical Eng, May 2023, p. 11. doi: 10.1117/12.2678898.
[2] Wilson Research Group, “2024 IC/ASIC Functional Verification Trend Report,” 2024. https://resources.sw.siemens.com/en-US/white-paper-2024-wilson-research-group-ic-asic-functional-verification-trend-report/
[3] ARM Limited, “ARM Cortex-A9 processors Software Developers Errata Notice,” 2015. [Online]. Available: https://developer.arm.com/documentation/uan0008/latest
[4] Clark and Peter, “Intel has late metal fix for design error,” EE Times. Accessed: Jul. 07, 2025. [Online]. Available: https://www.eetimes.com/intel-has-late-metal-fix-for-design-error/
[5] Nicely and T. R., “Pentium_FDIV_flaw-lessons_learned,” IEEE Micro, vol. 15, no. 6, pp. 86–93, 1995, doi: 10.1109/40.465185.
[6] LUBIS EDA, “Industrial Case Studies Common Blocks Rate Limiter,” 2024.
[7] LUBIS EDA, “LUBIS EDA Consulting Fast, Reliable and Bug-Free.” [Online]. Available: www.lubis-eda.com