Decoding Formal 
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 » Verification Management from a Formal PerspectiveFebruary 18th, 2014 by Dr. Jin Zhang
Recently, Gabe Moretti, contributing editor to Chip Design, wrote a lengthy article for Systems Design Engineering addressing an important topic, “Verification Management.” It included comments from Atrenta, Breker Verification Systems, Jasper Design Automation, Mentor Graphics, OneSpin Solutions, Oski Technology and Sonics on a series of questions from Gabe on how to manage today’s complex and time-consuming verification process. Read the rest of Verification Management from a Formal Perspective Serving a Need in the Formal CommunityFebruary 3rd, 2014 by Dr. Jin Zhang
Oski Technology launched the quarterly Decoding Formal Club with the goal of creating an industry-wide, independent platform for all formal enthusiasts to share ideas, challenges and solutions so as to advance formal technology and promote formal sign-off in the industry. On Jan. 23rd 2014, we had our second meeting in the Computer History Museum. 28 formal enthusiasts (many of them formal experts) gathered from 16 different companies including ACM, Broadcom, Cadence, Chelsio, Cisco, Ericsson, Ikanos, Jasper, MediaTek, Mentor Graphics, Microsoft, NVIDIA, Qualcomm, SMI, Synopsys and a stealth startup. Talks were given by Normando Montecillo from Broadcom on data integrity verification and Vigyan Singhal, Oski CEO, on Abstraction Models. It was a very successful event as demonstrated by the anonymous survey results. Answers to the question “What are your primary goals for attending the event?” reinforced the original intention of the group’s founders, that is to facilitate knowledge sharing and networking among formal experts. Read the rest of Serving a Need in the Formal Community The Abstraction Model – Is It More, Is It Less?January 22nd, 2014 by Dr. Jin Zhang
Oski Technology provides formal verification services to leading semiconductor companies to verify complex design blocks that are difficult to verify using simulation. In our projects, we often write Abstraction Models to overcome formal complexity barriers that would otherwise render formal verification results inconclusive. For example, for the open-source Sun OpenSparc T1 design, verifying a data transport checker without the Abstraction Models would have taken an estimated 991 days of run-time, but only 147 seconds with the Abstraction Models, a significant speed-up of 600,000X. With Abstraction Models and other similar techniques, formal verification can be used as sign-off criteria in the verification flow; Oski has helped many customers adopt and develop formal sign-off flows. Customers often have the misconception that Abstraction Models reduce design behaviors which makes the formal verification task easier and allow it to finish sooner. They worry about missing bugs with Abstraction Models. In reality however, Abstraction Models do not reduce design behaviors; to the contrary they add to design behaviors by adding new reset states, and/or state transitions. As a result, no bug will be missed. More is less because when more behaviors are added purposefully and artfully, they can actually make the formal verification job easier for the tools and take less time. This might be counter-intuitive and may take some time and practice to get used to. But if one understands the concept and techniques of writing and using Abstraction Models, formal verification can be put to much better and broader use. Because each design is different, custom Abstraction Models are needed for each design. There is no Abstraction Model VIP one can purchase to fit all kinds of designs. The good news is that knowing when and how to use Abstraction Models is very much a teachable, learnable skill. We teach our customers about Abstraction Models in our projects and we include the Abstraction Models we develop for the project as source code so customers can write their own Abstraction Models in future projects. Now is your opportunity to learn more about abstraction models. Vigyan Singhal Oski CEO, will be presenting a talk on Abstraction Models in the upcoming Oski Decoding Formal Club event on Jan. 23rd, 2013 in Mountain View, CA. The talk will cover what Abstraction Models are, when you need them, how to write them and how to use them, using real examples. Space is limited, so don’t miss this opportunity to come and learn more about Abstraction Models so your formal verification runs will take less time. Register for Oski Decoding Formal Club event on Jan. 23rd, here. Event: Decoding Formal Club meeting For Abstraction Models, More is Less! Oski Innovation Enables Formal Sign-Off in 2013December 19th, 2013 by Dr. Jin Zhang
A busy year is drawing to a close for Oski Technology. Reflecting back on this year we are proud of what we have accomplished for our valued customers. Oski Formal Sign-off Methodology, incorporating End-to-End checkers, Abstraction Models and formal coverage – this is the boldest application of formal technology for RTL functional verification. Gone are the days when formal can only be used to compliment simulation on a given block. Oski Formal Sign-off Methodology and formal verification can replace block-level simulation for suitable designs to improve overall verification coverage, efficiency and productivity. The logic is simple – control and data transport types of blocks and designs with complex corner scenarios are better suited to be verified with formal than simulation. We have applied such methodology to tapeout many of our customers’ mission-critical projects and at the same time develop formal expertise in our customer base. Read the rest of Oski Innovation Enables Formal Sign-Off in 2013 Promoting Formal Education: Oski Shares Experiences at FMCAD 2013November 25th, 2013 by Vigyan Singhal
Although Oski Technology is first and foremost a formal verification service company, making effective use of formal tools and promoting education around the power of formal technology has always been at the core of our business. Since Oski was founded in 2005, we have engaged in many activities to help increase the adoption of formal in the industry: 1. Our formal verification service offering includes training for customers on End-to-End formal verification and Oski Formal Sign-off Methodology so they can leverage formal effectively and across all design projects. 2. We produced the “Decoding Formal” series of video tutorials on formal verification covering a broad array of topics and interests, and made the series available on the Oski website. Read the rest of Promoting Formal Education: Oski Shares Experiences at FMCAD 2013 Oski’s Two New Secure Chambers Support Asia GrowthNovember 6th, 2013 by Rahul Joshi
Oski Technology, founded by Vigyan Singhal, pioneer and practitioner in formal verification, has earned great respect and reputation in the Silicon Valley for helping customers tape out mission-critical projects using formal technology. Leveraging the power of End-to-End formal verification and Abstraction Models, Oski works with its customers to adopt formal sign-off methodology so that formal verification can become part of the verification sign-off flow. Read the rest of Oski’s Two New Secure Chambers Support Asia Growth Oski Technology: Bullish on Formal VerificationOctober 2nd, 2013 by Nanette Collins
Oski Technology may be named for the famous University of California at Berkeley’s bear mascot, but Oski is not bearish at all on the formal verification market. In fact, it’s downright bullish on this form of verification and its importance to chip design. One recent morning, Vigyan Singhal, Oski’s president and CEO, was in the Mountain View, Calif., corporate headquarters ready to discuss his life in formal verification and what inspires him and the company he founded. Read the rest of Oski Technology: Bullish on Formal Verification Why Formal Can’t Scale without MethodologySeptember 12th, 2013 by Vigyan Singhal
Formal verification, and in particular model checking, has been around for a few decades now. I found my first post-silicon bug using formal 20 years ago at Motorola Austin in the cache controller block of a PowerPC chip. The power of formal technology drove my Ph.D research and subsequent career in formal verification. Early on in my career, I focused on developing formal verification tools at Cadence. Later, I founded Jasper and did more of the same. Over the years however, despite the continuous improvement of formal technology, I find that formal adoption has been less than stellar. In particular, I feel people are not harnessing the full power that formal tools can provide. What is needed besides good tools is a scalable methodology. Methodology is a body of practices, procedures, and rules used in a discipline. In simulation, both open source methodologies e.g. OVM (open verification methodology), UVM (universal verification methodology) and proprietary verification methodologies, internally developed by design teams of a company, exist. These have been of great help to the design and verification communities, which help scale simulation to keep up with the ever increasing complexity of the designs. Calling All Formal Enthusiasts: Join the Oski “Decoding Formal” ClubAugust 15th, 2013 by Vigyan Singhal
In our years of providing formal verification services to leading-edge semiconductor companies, I have had the pleasure of meeting and working with many smart and dedicated engineers who paved the way of formal adoption in their companies – studiously applying formal technology to verify more complex designs as well as building up formal methodology so formal can become part of sign-off criteria in their verification flow. I have had countless discussions with these individuals on the nature of formal technology, best practices in formal application, and ways of getting the most out of formal tools in verification. These are valuable mutual learning experiences for all of us. In working with these formal technologists and practitioners, I have always wanted to create a forum for these kindred spirits – formal enthusiasts, pioneers, leaders and friends who work in different companies but on the same mission. The goal is to promote idea sharing among us so together we can further advance formal technology and broaden formal adoption in the industry. Read the rest of Calling All Formal Enthusiasts: Join the Oski “Decoding Formal” Club IP Customers Beware! “Silicon Proven” IP May Not Be Fully VerifiedJuly 26th, 2013 by Prashant Aggarwal
The verification of all configurations (reaching in millions) of an (silicon) IP is a challenge. I have experienced this problem first-hand both from the vendor side as an embedded SRAM (eSRAM) compiler designer, and from the customer side, as an architect of a wireless SoC using 3rd party IPs. When I was eSRAM compiler designer, eSRAM used to support hundreds of thousands of configurations based on address widths, data widths, data masking, low power features, etc. In order to meet performance for different configurations, I sometimes designed different internal architectures of eSRAMs for different configurations. Due to the large number of configurations, verification is performed only on the configurations where the designer identifies the greatest need, for example when there is an architecture change either in the design or layout. Though this approach may appear to be comprehensive, I have seen silicon failures because the configurations picked for silicon had not been verified. The failures were due either to design modeling error or layout programming error. These failures could have been caught at the verification stage, if all configurations of eSRAMs were verified. However using simulation as the sole verification technology, verifying all configurations was simply not possible. Read the rest of IP Customers Beware! “Silicon Proven” IP May Not Be Fully Verified |
|
|
|||||
|
|
|||||
|
|||||
