Formal verification best practices: towards end-to-end properties
In the first two episodes of this blog series, we saw how we put in place an efficient formal testbench for a cache, how we found a genuine bug, reproduced a deadlock bug and found a design fix. At this point we were confident that no other deadlock bug exists. This episode shows how we verified powerful assertions, and how we prepared the formal testbench to verify end-to-end properties (an end-to-end property checks the DUT outputs against what has been seen on its inputs), along with new best practices.
An essential property
Actually, let’s start with a property that is not end-to-end but that is essential for a cache. This property is the only one we will have to check internal details. It verifies that, upon a hit request in the cache, the hit is in only one way. If that is not respected, there is a strong ambiguity about which data to read or write.
hit_onehot: assert property(i_ucache.i_hit_stage.is_hit |-> $onehot(i_ucache.i_hit_stage.hit_way);
When a lookup is performed in the cache, the address is split into a tag (123 in the following figure), an index (1), and an offset. The index is used to address tagram ways. If the content of this index is valid and the tag is the same in two ways (0 and 2 below), this is a “multiple hit”, and a serious problem. Many potential design bugs can be seen as a violation of this property.
To read the full article, click here
Related Semiconductor IP
- MIPI I3C Master RISC-V based subsystem
- ISO26262 ASIL-B/D Compliant 32-bit RISC-V Core
- RISC-V CPU IP
- RISC-V Vector Extension
- RISC-V Real-time Processor
Related Blogs
- Formal verification best practices to reach your targets
- Formal verification best practices: investigating a deadlock
- Formal verification best practices: checking data corruption
- Formal verification best practices: sign-off and wrap-up
Latest Blogs
- Rivos and Canonical partner to deliver scalable RISC-V solutions in Data Centers and enable an enterprise-grade Ubuntu experience across Rivos platforms
- ReRAM-Powered Edge AI: A Game-Changer for Energy Efficiency, Cost, and Security
- Ceva-XC21 and Ceva-XC23 DSPs: Advancing Wireless and Edge AI Processing
- Cadence Silicon Success of UCIe IP on Samsung Foundry’s 5nm Automotive Process
- Empowering your Embedded AI with 22FDX+