Dr. Jin ZhangJin Zhang has over 15 years of experience working in EDA, driving the effort of bringing new products and services to market. At Oski Technology, she is responsible for Oski’s overall marketing strategy as well as business development in Asia Pacific. Prior to that, she was the General Manager at EVE-China, and Director of Technical Marketing at Real Intent. She has also worked at Cadence Design Systems and Lattice Semiconductor Corp. Jin has a PhD in logic synthesis and verification and a Master’s degree in International Management focusing on Asia Pacific.
« Less
Dr. Jin ZhangJin Zhang has over 15 years of experience working in EDA, driving the effort of bringing new products and services to market. At Oski Technology, she is responsible for Oski’s overall marketing strategy as well as business development in Asia Pacific. Prior to that, she was the General Manager at
… More »
Not Far from Formal to Success
October 7th, 2014 by Dr. Jin Zhang
Several acquisitions this year caught my attention, and show the strategic importance of formal verification for chip design.
Proving that formal verification matters, Jasper Design Automation (founded by Oski CEO Vigyan Singhal) was recently acquired by Cadence Design Systems in June, for $170 million. It is worth noting that Cadence has a long history of acquiring formal verification tool companies:
- Cadence acquired Bell Labs’ EDA Group along with its FormalCheck Model Checker in 1998.
- Cadence acquired Verplex in 2003 with its Conformal Equivalence Checker and BlackTie Model Checker.
- Cadence is soon to integrate the JasperGold suite of formal tools and applications.
These acquisitions underscore Cadence’s understanding of formal verification and its commitment to formal technology.
While not every chip design company recognizes the benefits of formal verification, those who do, set themselves apart, and are successful. Two Oski customers serve as examples of this phenomenon:
- Cavium acquired XPliant in July 2014, a startup providing high-performance, high-density switch silicon targeting a broad range of switching applications for the data center, cloud, service providers and enterprise market. XPliant had been operating in stealth mode but has become a poster child for formal adoption.
Since XPliant’s switch design is fully configurable and flexible, it is impossible to verify all configurations using simulation. In addition, being a startup means resources and schedule are at a premium. Formal was a natural choice due to its exhaustiveness to cover all configurations, and its ability to find bugs early to save overall verification time.
When Oski first engaged with XPliant, we were given only a few blocks to verify. Within days of deployment, formal began to show value and started reporting bugs. The results from formal were so convincing that over the course of our one-year engagement, the scope of formal verification was expanded several times to include more and more blocks. By the end of the project, almost half of the RTL code was completely verified using formal. For a start-up building a highly configurable ASIC that would be otherwise impossible to verify with simulation in the limited time-to-market they had, this is a remarkable testimonial that formal can be a dominant tool in one’s verification flow.
- Cisco announced its acquisition of Memoir Systems in September 2014. Memoir is a company developing semiconductor memory IP with faster memory access speed, and a smaller overall footprint. Memoir has been using formal verification to verify its configurable memory IP. Memoir co-founder and COO Da Chuang has been an advocate of formal technology used by verification engineers for IP verification, and designers during the design process, to find bugs early. Oski has worked with Memoir since its founding in 2009, and we are not surprised to see its innovation and efforts paid off.
These acquisitions further reinforce the fact that formal is an integral part of the success of these companies.
Oski Technology takes pride in helping our customers reach success through formal application and adoption. In 2013, Oski created the industry-wide Decoding Formal Club, with the goal to share formal knowledge and experience. Thus far the Club has been a lively forum for talks on formal sign-off methodology, achieving sign-off with bounded proof or abstraction models and building a formal test plan for sign-off.
The next Decoding Formal Club meeting will be held on Thursday, October 23, at the Computer History museum. Synopsys is sponsoring this event.
- Vigyan Singhal will present another important topic related to formal sign-off ––End-to-End checkers. The presentation will explain what they are, and how to write them efficiently to achieve formal sign-off.
- Syed Suhaib, CPU and Tegra formal verification team manager at NVIDIA, will share insights on his team’s real-world formal experience in verifying the recently announced NVIDIA Denver CPU.
- Robert Kurshan, a noted formal verification pioneer, will talk about formal verification of cache coherence. He will cover its history and discuss actual requirements and practical options for verifying memory consistency using a model checker.
We hope you can join us for insightful talks, “formal” networking, museum tours, gifts and Indian food to celebrate Diwali. By joining us, you will be another step closer to success.
Pre-registration is required. To register, please visit: http://tiny.cc/ea6zmx
Related
Tags: cache coherence, formal verification, processor verification, Robert Kurshan, Vigyan Singhal
Category: Blog
This entry was posted
on Tuesday, October 7th, 2014 at 6:28 am.
You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.
