Decoding Formal Archive for the ‘Blog’ CategoryBuilding Up the Formal CommunityTuesday, April 8th, 2014In our visits to many of our customers in the past year, we received a few common requests from companies both large and small:
Oski Receives DVCon “Honorable Mention” for Best Paper on Bounded ProofsThursday, March 20th, 2014DVCon 2014 was a terrific show for Oski Technology. Not only were we proud to receive an “Honorable Mention” for (2nd) Best Paper at DVCon “Sign-off with Bounded Formal Verification Proofs”, we had the opportunity to have many meaningful conversations with existing customers and others new to formal verification and eager to learn more about what is possible with formal verification. Our DVCon “Sign-off” paper is available on the Oski Technology Web site. See our DVCon 2014 video here.
Countdown to DVCON 2014Friday, February 28th, 2014The countdown to DVCON 2014 has begun! With more exhibitors and attendees than ever before, new programs and technical sessions, longer exhibit hours, DVCON 2014 is shaping up to be another outstanding event for the industry. At Oski Technology, we are excited to offer many opportunities to connect with verification experts in the industry at DVCON – share ideas, discuss problems and solutions related to formal technology and formal sign-off methodology. • Monday March 3rd 5:00 – 7:00pm, Oski will join the inaugural DVCON Booth Crawl and offer healthy stacks – nuts, veggie sticks and wine, while we enjoy great conversations. Come and chat at the Oski booth #305. (more…) Verification Management from a Formal PerspectiveTuesday, February 18th, 2014Recently, 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. Serving a Need in the Formal CommunityMonday, February 3rd, 2014Oski 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…) The Abstraction Model – Is It More, Is It Less?Wednesday, January 22nd, 2014Oski 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 2013Thursday, December 19th, 2013A 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. Promoting Formal Education: Oski Shares Experiences at FMCAD 2013Monday, November 25th, 2013Although 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. (more…) Oski’s Two New Secure Chambers Support Asia GrowthWednesday, November 6th, 2013Oski 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. (more…) Why Formal Can’t Scale without MethodologyThursday, September 12th, 2013Formal 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. |
|||||
|
|
|||||
|
|||||
