Memoir Systems design high performance and highly configurable memory IP cores. Formal verification has always been an important strategy to ensure functional correctness of its configurable memory IPs, as it is hard to cover all configurations using simulation. Due to the complex nature of Memoir Systems’ design, Oski Technology is involved to help identify formal verification complexity spots and craft solutions to overcome the complexity challenge. Due to Oski’s engagement, the memory IPs from Memoir Systems are formally verified and exhaustively proven – 100% verified. (Update: Memoir was acquired by Cisco in September 2014.)
DAC 2012 Oski Verification Challenge: Oski took a NVIDIA design unseen and formally verified it in 72 hours and found 4 corner case bugs. This shows the power of formal technology in the hands of formal experts with the right methodology in finding corner case bugs in a short time. See the Oski Technology blog, for photos and a recap.
- Deploying Model Checking for Bypass Verification Read full story
- End-to-End Formal using Abstractions to Maximize Coverage Read full story
- How Formal Methodology Shrank the Verification Schedule of a Complex Statistics Block by 6x Read full story