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
- Temperature Glitch Detector
- Clock Attack Monitor
- SoC Security Platform / Hardware Root of Trust
- SPI to AHB-Lite Bridge
- Octal SPI Master/Slave 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