Posts Tagged ‘formal verification’
Monday, February 3rd, 2014
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. (more…)
Tags: "Decoding Formal" Club, formal sign-off, formal verification
2 Comments »
Wednesday, January 22nd, 2014
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
Date: Thursday January 23, 2014
Time: 1:00 PM – 3:30 PM
Venue: Mountain View, CA.
For Abstraction Models, More is Less!
Tags: "Decoding Formal" Club, Abstraction Models, formal sign-off, formal verification, formal verification methodology
No Comments »
Wednesday, October 2nd, 2013
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. (more…)
Tags: "Decoding Formal" Club, #50DAC, assertion-based verification, Decoding Formal, Deep Formal Award, end-to-end checkers, FMCAD, formal sign-off, formal verification, formal verification methodology, formal verification services, Oski Technology, Oski Verification Challenge, Rahul Joshi, Vigyan Singhal
2 Comments »
Thursday, September 12th, 2013
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.
(more…)
Tags: formal verification, Vigyan Singhal
2 Comments »
Friday, July 26th, 2013
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.
(more…)
Tags: 3rd party IP, EDA, end-to-end checkers, formal verification, Formally Certified IP, formally verify highly configurable IP, IP re-use, third-party IP, verify IP, VIP
No Comments »
|
