Formal verification best practices: checking data corruption
If you are joining me now in this formal verification blog series, welcome! In episode 1, we looked at best practices to set up formal verification on a specific component. In episode 2, we focused on the verification of a deadlock bug. In episode 3, we spent time setting up the formal testbench for end-to-end properties. In this episode, let’s focus on data corruption.
End-to-end assertions for data checking
We are now almost ready to verify two new major assertions (and their derivatives). Without knowing anything about the design microarchitecture, we can still write these assertions.
- After a write request to an address A, with a data D, the following read request to A will return D. This must be true regardless of each request hitting or missing in the cache. The line holding A may even be evicted between the two requests.
- Two consecutive read requests to the same address return the same data.
Interestingly, at that point a new bug was found in the design by simulation, caused by the fix for the deadlock discussed in the second episode. It was not found by FV so far, because it is a data corruption bug while our formal testbench was only able to catch control bugs. So let’s fix that.
To read the full article, click here
Related Semiconductor IP
- Process/Voltage/Temperature Sensor with Self-calibration (Supply voltage 1.2V) - TSMC 3nm N3P
- USB 20Gbps Device Controller
- SM4 Cipher Engine
- Ultra-High-Speed Time-Interleaved 7-bit 64GSPS ADC on 3nm
- Fault Tolerant DDR2/DDR3/DDR4 Memory controller
Related Blogs
- Formal verification best practices to reach your targets
- Formal verification best practices: investigating a deadlock
- Formal verification best practices: towards end-to-end properties
- Formal verification best practices: sign-off and wrap-up
Latest Blogs
- Shaping the Future of Semiconductor Design Through Collaboration: Synopsys Wins Multiple TSMC OIP Partner of the Year Awards
- Pushing the Boundaries of Memory: What’s New with Weebit and AI
- Root of Trust: A Security Essential for Cyber Defense
- Evolution of AMBA AXI Protocol: An Introduction to the Issue L Update
- An Introduction to AMBA CHI Chip-to-Chip (C2C) Protocol