Dr. Jin Zhang
Jin 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 »
February 3rd, 2015 by Dr. Jin Zhang
Last year, after my presentation to a customer in Asia, the verification manager said, “You should give this talk to our senior executives, so they understand the benefits of formal.”
It was said in a lighthearted manner, but in reality it rang true. Design and verification engineers and their managers understand the value of formal. However in order to request funding to promote formal adoption, they still need to make a case to senior executives as to the value of formal. They need compelling arguments, speaking at a strategic level as to why it is critically important and urgent for the company to adopt formal. The list of concerns for senior executives, is long:
Funding will become easier, if they understand how formal can address their primary concerns.
To stay ahead of competition not only requires innovative ideas, but also a sharpened toolkit. Semiconductor companies large and small are actively investing in formal adoption so that they have the best verification flow with the most advanced tools and methodologies. There aren’t many formal experts who can do End-to-End formal in the industry. Many companies are paying top dollar to attract formal verification engineers or outsource formal verification tasks for critical projects to the Oski Technology. So if your company doesn’t use formal verification, then this is an easy case to make, in order to catch up with competition.
A post-silicon bug is a nightmare to senior executives. It signifies poor quality, delayed schedule and wasted money. No matter how complex the bug might be at the system level, it resides in one of the design blocks and could have been caught earlier. Using End-to-End formal to achieve sign-off is a sure way to catch corner case bugs early in the flow so as to minimize, or even avoid, post-silicon bugs. So if senior executives are concerned about customer issues with products, the best solution is to incorporate formal in the early stage, for sign-off.
Time is money. Delayed project schedule means extra engineering time and lost potential market opportunity. Formal can reduce project schedule as in the Oski Cisco case study, published at DAC 2011. At the very least with formal, once a property is proven, verification is done. Unlike simulation where reaching the last 20% of coverage closure could take 80% of the time, so there is never a real sense of being complete as it is impossible to simulate all input vectors.
So if adding formal to the flow helps you keep up or stay ahead of competition, avoid post silicon bugs and keep your project schedule in check, it has a big impact for the company. This should make a strong case to senior execs that formal is something they should hear about – and sponsor – today.
Rob Kurshan, early pioneer and expert in formal verification, speculates here on the future of formal verification in a video interview at a past meeting for the Decoding Formal Club, a forum hosted by Oski Technology for formal enthusiasts, pioneers, leaders and colleagues who work to promote the sharing of ideas and the advancement of formal technology. On February 9 Synopsys is sponsoring the next Decoding Formal Club Meeting about constraints, liveness vs. safety, formal at ARM (and a Klein bottle). Space is limited and pre-registration is required. Sign up here.
January 16th, 2015 by Dr. Jin Zhang
According to statistics published in 2014 by the University of Scranton in Pennsylvania in the Journal of Clinical Psychology, 45% Americans usually make New Year’s Resolutions. And people who explicitly make resolutions are 10 times more likely to attain their goals than people who don’t.
The largest resolution category –– 47%, is related to self-improvement and education. This is me, trying to squeeze time in my busy schedule to work out and keep my brain sharp by learning new things. This year, our family joined a new health club where I can watch TED Talks as I walk, and I am embarking on a learning journey with my sixth grader on Machine Learning & Robot Design. It has been fun!
As the Director of Marketing at Oski Technology, my New Year’s Resolution for Oski is simple –– Treading Deep into Formal. In the past 18 months, we successfully hosted five Decoding Formal Club events where we, and our invited guests, shared some of the deepest knowledge and practical experiences about formal that cannot be found elsewhere.
We have covered many deep formal topics such as Abstraction Models, Bound Analysis, End-to-End Checkers, and Formal Test Planning, all with the goal to achieve Formal Sign-off. Invited guests from industry formal leaders, such as NVIDIA and Broadcom, shared their experiences deploying formal. With deep formal talks, opportunities for formal networking, good food and cool gifts, Decoding Formal Club has become a magnet that attracts formal enthusiasts. It is where deep formal learning happens.
Carrying on the theme of Treading Deep into Formal into 2015, our first Decoding Formal Club meeting will be held Monday, February 9, from 11:30 a.m. until 4:15 p.m. at our usual location, the Computer History Museum in Mountain View.
We have an agenda packed with Deep Formal Talks and lots of fun! It will include talks by:
While attendees tread deeply into the formal space, we will bring them back with a special invited guest Cliff Stoll. His TED Talk, “The Call to Learn” inspired us to offer one of his Acme Klein Bottles as a giveaway. And with the Chinese New Year coming February 19, attendees will be in for Chinese flair and other surprises.
The event space can hold only 40 people, and we intentionally keep the event small to offer the best learning and networking experience. Our goal is to make it the best four hours of an attendee’s work week.
Come and join us as we Tread Deep into Formal in 2015. It will be exciting!
Visit the Decoding Formal registration page, here.
December 22nd, 2014 by Pippa Slayton
2014 has been an exciting year for advances in technology, and another successful year for Oski Technology.
Applying formal verification technology to the most challenging formal verification problems has been at the core of Oski’s business for nearly 10 years, and in 2014 we continued this journey with customers and partners from more than a dozen companies, many of which are in the top 10 performers in the industry. We expanded our business in Asia by more than 5x, at many new companies whose managers are extremely judicious about where money is being spent in their verification effort.
We continue to balance growth in our customer base with a commitment to advancing the application of formal verification in the industry, by teaching the “how”, as we go. In 2014 we offered advanced formal sign-off training to many of our customers, and have received overwhelmingly positive feedback about how this program has helped these teams navigate the complexity of applying formal verification.
Another important aspect of our commitment to the advancement of the application of formal verification is the user-focused Decoding Formal Club which started out as the Decoding Formal video tutorial series, launched at DAC in 2013. The goal of the Decoding Formal Club is to foster knowledge-sharing about the use of formal verification within the industry. The past few years have seen explosive growth and interest in these events, where we have discussed a range of practical topics of special interest to formal verification engineers, including a popular panel “How to Build a Productive Formal Team” addressing an important question for every manager tasked with adopting formal verification.
We took our June Decoding Formal Club meeting to DAC in San Francisco, in the form of a two-hour DAC Insight tutorial focused on the application of formal test planning, and why it is key to formal sign-off. The most popular videos show highlights from each presentation: “Formal Test Planning”, “Formal Test Planning: Case Studies”, and “Abstraction Models”. Video for the latest event in October 2014, “Formal Talks: Methodology, Application, Real-World Experience”, is here.
The Decoding Formal Club welcomed an impressive array of guest speakers and panelists this year, including Normando Montecillo from Broadcom, Flemming Anderson from Intel, Da Chuang from Memoir Systems (since acquired by Cisco), Prosenjit Chatterjee from NVIDIA, Joanne Ottney from Palo Alto Networks, Syed Suhaib from NVIDIA, and Bob Kurshan, a pioneer of formal verification.
The future for formal verification looks bright, and those at the forefront continue to be optimistic about 2015 and beyond. Bob Kurshan, presenter, states in an interview at the Decoding Formal Club meeting in October 2014, that while there will always be room for simulation, formal will one day be the “workhorse” of verification; others are in strong agreement. Short video interviews featuring Bob Kurshan, Brian Bailey (Semiconductor Engineering), Richard Newton (Ericcson), Kaowen Liu (MediaTek) and Shiva Borzin (OneSpin), and Jin Zhang (Oski Technology), are here. The next meeting is scheduled for February 9, 2015, details to be announced; subscribe here.
With another year behind us, we remain optimistic about the rate at which formal technology is being advanced and adopted. The technology has never moved so fast, as is true of its practical application, especially in the area of end-to-end formal which replaces simulation for verification sign-off. This is an exciting period to be working with formal. We are past the point of no return. As the European Space Agency (ESA) announced during the Rosetta mission, after the Philae lander was released for its trip to the surface of comet 67P, “There’s no going back now.”
Prospects are good that 2015 will be better than ever for technological advances of all kinds. And what better time to say it. “There’s no going back now.”
Happy holidays and best wishes for the New Year!
P.S. Decode the binary message in the our holiday card (or below), and reply to us at 67P @oskitech.com
01001000 01100001 01110000 01110000 01111001 00100000 01001000 01101111 01101100 01101001 01100100 01100001 01111001 01110011 00100001
November 10th, 2014 by Pippa Slayton
What if all design and verification engineers used formal? What if formal tools become smart enough to do the abstractions? What if formal tools had infinite capacity? These and other questions were proposed by attendees on the event survey for this quarter’s Decoding Formal Club event on October 23, 2014 at the Computer History Museum in Mountain View, CA. Read the rest of “What if” All Design and Verification Engineers Used Formal?
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. Read the rest of Not Far from Formal to Success
September 18th, 2014 by Dr. Jin Zhang
You might still be skeptical of the idea that formal verification can be used by everyone. After all, there is a deep-rooted perception in the industry that formal verification is for the elite few formal experts with Ph.Ds.
This might have been true in the early days of formal technology. The formal tools’ capacity was limited and the use model was not mature. So the aid of someone who actually understood the algorithms “under the hood” was important to help the tool solve the tasks at hand.
However, things have changed dramatically in the last decade. Read the rest of Formal Verification, by Everyone and for Everyone
August 27th, 2014 by Dr. Jin Zhang
Brian Bailey’s recent article on “Fixing Functional Coverage” in Semiconductor Engineering (http://semiengineering.com/fixing-functional-coverage/) polled experts from different companies about the challenges of catching all the bugs, utilizing assertions and expanding coverage to the entire system. This blog elaborates on the four points we made in Brian’s article about how formal can help with functional coverage. Read the rest of Using Formal for Functional Coverage
August 13th, 2014 by Dr. Jin Zhang
The Hardware Model Checking Competition (HWMCC) was conceived at CAV (Computer-Aided Verification) 2006 and first launched at CAV 2007. The goals were to encourage technical advancement of model checking algorithms and thereby their deployment in the industry to promote formal adoption for hardware design verification. Read the rest of Sponsoring Technical Advancement in Formal Verification
June 19th, 2014 by Dr. Jin Zhang
This year at DAC, a question asked repeatedly got our attention: Do you offer advanced formal training program?
While we are not surprised by the request itself, the number, size, type and location of companies that asked about this was surprising. It included a wide spectrum of companies, from the U.S., Japan, Korea, China, along with large companies with established formal teams as well as small start-ups with no formal experience. Even EDA vendors asked if we could do training for them. Read the rest of Formal Training in High Demand
June 13th, 2014 by Dr. Jin Zhang
This year at DAC, we asked attendees to participate in a guessing game – make an educated guess about how long it takes to formally verify a design based on the given design description and statistics.
Here is a recap of the information provided to participants: