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
- eDP 2.0 Verification IP
- Gen#2 of 64-bit RISC-V core with out-of-order pipeline based complex
- LLM AI IP Core
- Post-Quantum Digital Signature IP Core
- Compact Embedded RISC-V Processor
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
- Enhancing PCIe6.0 Performance: Flit Sequence Numbers and Selective NAK Explained
- Smarter ASICs and SoCs: Unlocking Real-World Connectivity with eFPGA and Data Converters
- RISC-V Takes First Step Toward International Standardization as ISO/IEC JTC1 Grants PAS Submitter Status
- Running Optimized PyTorch Models on Cadence DSPs with ExecuTorch
- PCIe 6.x: Synopsys IP Selected as First Gold System for Compliance Testing