Normando Montecillo, Associate Technical Director at Broadcom, shared his success story on how he became a full time formal engineer and chartered the “Center for Excellence” group to promote formal adoption and proliferation across different groups at Broadcom.


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.


  1. Deploying Model Checking for Bypass Verification Read full story
  2. End-to-End Formal using Abstractions to Maximize Coverage Read full story
  3. How Formal Methodology Shrank the Verification Schedule of a Complex Statistics Block by 6x Read full story


Formal property verification (also known as model checking) is a powerful methodology that can be used to find corner-case bugs, improve verification efficiency and reduce the verification cycle. However, inconclusive formal analysis results or bounded proofs have been hindering adoption of formal technology in the industry. This paper describes a formal sign-off methodology in the presence of bounded proofs. With an understanding of the design-under-test and a systematic analytical approach, we can qualify the bounded proof depths and use Abstraction Models to achieve the required proof bound for formal sign-off. Read full story