Bridging the Gap: When Formal Verification Catches What Simulation Misses

In the intricate world of semiconductor design verification, the interplay between formal verification and simulation-based approaches continues to evolve. A recent case study highlights the complementary nature of these methodologies and underscores the importance of a comprehensive verification strategy.

The Scenario

During a routine IP verification using formal tools and SystemVerilog Assertions (SVA), a bug was uncovered that had previously eluded detection in subsystem-level simulation. This discovery prompted a deeper investigation into the verification process and the tools employed.

Formal Verification's Unique Strength

Formal verification's ability to exhaustively explore state spaces within specified bounds allowed it to uncover a corner case that simulation had missed. This strength stems from formal tools' capacity to:

  1. Examine all possible states and input combinations
  2. Operate without the need for specific test vectors
  3. Explore deep states that might be challenging to reach through simulation alone

Bridging Formal and Simulation

To leverage this formal verification insight in the simulation environment, the team converted the formal traces (counter-examples) into SVA cover sequences. We at AsFigo develop and deploy such apps for customers (one such example is Waves2UVM). 

This innovative approach allowed them to:

1. Create targeted checks for specific scenarios uncovered by formal verification

2. Run these sequences against existing simulation dumps to identify which tests, if any, covered the problematic scenario

Unexpected Findings

Upon analyzing 1000+ simulation dump files with the new cover sequence, an intriguing result emerged: 32 tests actually covered the scenario in question. This revelation led to a critical question: Why didn't these tests fail if they encountered the buggy scenario?



Investigating Silent Passes

Several factors could contribute to tests covering but not exposing the bug:

1. Incomplete checkers in the simulation environment

2. Assertions were turned off in these tests ($assertoff/TCL commands)

Path Forward

 To resolve this discrepancy and strengthen the verification process, the team outlined several steps:

1. Enhance simulation checkers based on formal properties

2. Perform detailed timing analysis of simulation runs

3. Isolate the scenario in focused test cases

4. Review and align constraints between formal and simulation environments

Conclusion

This case study illustrates the value of integrating formal verification and simulation approaches. By converting formal insights into simulation-compatible checks, verification teams can:

1. Identify coverage gaps in simulation test suites

2. Create more robust, targeted tests

3. Improve bug detection and reproduction capabilities

As chip designs grow more complex, such synergistic approaches become increasingly crucial. By leveraging the strengths of both formal and simulation methodologies, verification teams can build more comprehensive and efficient verification strategies, ultimately leading to higher quality semiconductor designs.

Comments

Post a Comment

Popular posts from this blog

Opensource testbench generator for VHDL designs, OSVVM included!

Image
VHDL holds a prominent position in the world of FPGA design, particularly within the military, aerospace, and defense sectors. It serves both as a Register Transfer Level (RTL) design language and as a tool for creating testbenches. The availability of open-source simulators, such as GHDL and NVC, alongside numerous free FPGA simulators and synthesis tools, has provided FPGA designers with a significant advantage over their SystemVerilog counterparts. While the Universal Verification Methodology (UVM) is widely adopted among SystemVerilog users, VHDL practitioners have traditionally relied on various homegrown methodologies and frameworks. Recently, however, off-the-shelf methodologies and frameworks such as OSVVM, UVVM, and VUnit have become available to VHDL users. Each of these options presents different levels of complexity, allowing users to choose the one that best meets their needs. Despite these advancements, the development of open-source utility tools supporting the latest me...
Read more

Porting a complete UVC to Verilator + UVM - an anecdote!

Image
 So, here we are on Day-1 of UVM + Verilator becoming available to the public, start of democratizing chip design verification. In case you just woke-up/started on this topic, read the release of UVM + Verilator with some intricate details on the challenge on the way by Antmicro via:  https://antmicro.com/blog/2023/10/running-simple-uvm-testbenches-in-verilator/  Awesome work by the folks at Antmicro and fantastic support by the ecosystem specifically Western Digital, kudos!  At AsFigo , we are committed to fueling open-source driven chip design and verification. So we took this opportunity to port a commercial-grade UVC (Universal Verification Component or a Verification IP) and ported it to compile and run on Verilator. Below are our reflections from this experiment. Get in touch with us to discuss how AsFigo can help your VIPs and testbenches to be ported to opensource EDA.  Case study: VLBus - a simple peripheral bus intended for write/read to configuration...
Read more

Meet the team behind SystemVerilog Assertions Handbook

Image
The SystemVerilog Assertions Handbook The SystemVerilog Assertions Handbook is a popular publication in the field of hardware design and verification. Authored by Ben Cohen, Ajeetha Kumari, Srinivasan Venkataramanan, and Lisa Piper, it became the world’s first book solely dedicated to SystemVerilog Assertions (SVA) when it was first published in 2005. At a time when SystemVerilog was gaining widespread acceptance, the authors recognized the need for a focused resource that could demystify assertions and provide engineers with practical insights into their use in modern verification flows. Now in its fourth edition, the handbook has evolved in tandem with advancements in the SVA standard, making it an indispensable reference for both beginners and experienced verification engineers. What sets this book apart is its combination of theory and practical examples, offering real-world insights into the effective use of SVA for improving design verification quality....
Read more