Oski Technology: 72-hour Live Verification Challenge

This is a great story: Oski Technology decided to prove the validity and efficiency of Formal Verification, and proposed a public challenge for themselves at DAC – a 72-hour window of time in San Francisco whereby they would attack a design problem never before seen, analyze it, propose a verification plan, and execute on that plan between 5 pm on DAC Sunday and 5 pm on DAC Wednesday.

To get a design problem, Oski Technology put out a request for proposal to different companies. The design could be at any stage in development, but had to include the RTL and some level of specifications for what the architecture should do, as well as some simulations.

Among the 5 respondents, Nvidia’s suggested problem was the most appropriate: It was a design that was still not complete and needed verification. More importantly, Nvidia was not afraid to have possible bugs or flaws in the design made public, a sign of their own confidence. So at 5 pm on Sunday, June 3rd, the Oski Technology team opened the files provided by Nvidia.

I’ll let Vigyan Singhal, Oski Technology’s President and CEO, take the story from there in his own words. Vigyan and I spoke by phone on September 12th, the same day a 6-minute video of the whole process was made available by the company. [Here’s the link on YouTube.]

**********************

The challenge …

Per Vigyan Singhal: “We had gotten the design in advance from the verification manager at Nvidia, but couldn’t even look at the documentation until 5 pm on Sunday, let alone the RTL files. Then after we opened everything, we looked at the code and the design specifications and went from there.

“Initially during the first night and the next morning, we were mostly doing planning. As we learned more about the design, as is usual with this type of thing, we found some unexpected things. Some of the sub-modules were missing from the design. Nvidia had given us the simulation waves, however, so we could guess the functionality and from there wrote Verilog for those little modules.

“This sort of situation is not unique to us, and is far more complicated that you can ever imagine. Often these things are missing from designs that we need to work on and yet there’s no one at the client company to consult with – they’re away from the office or have moved on to another employer – so we know how to deal with it. And it was part of what we wanted to explore by running our public challenge at DAC, to illustrate that it’s a good strategy in formal verification not to specify everything in the beginning.

“So, by Monday morning, after a thorough analysis of the problem, we announced our verification plan and declared that in the 72 hours we had allotted ourselves, we would not have time to verify both the read and write paths – just the read path in the design.

“Meanwhile, in order to showcase our work, our efforts were being streamed live onto monitors in our DAC booth on the Exhibit floor. People were coming by our booth to look at our efforts, and then stopping by a later point to see how much progress we had made.

“A lot of people in our audience were themselves in the process of building formal testbenches for their own projects, so they understood the difficulties we were facing. They could see we had taken on an ambitious challenge, but also understood we were doing something meaningful to the people who attend DAC.

“For us, however, the challenge was a big roller coaster – a test of our blood pressure. We never actually stayed up all night, but the first day and a half were stressful. One of the engineers on our team was visiting from India, so our night was his day which helped somewhat.

“In the end, the challenge was a big success. We actually finished so much ahead of schedule – a full 24 hours early – we were all able to attend the DAC party on Tuesday night, and on Wednesday during the day were able to discuss our results with people who came by our booth who had been tracking our progress since Sunday.”

**********************

Lessons learned …

Vigyan Singhal continued: “I’ve been coming to DAC for 20 years and know a lot about how to prepare for demos in the booth. Among the rules: Keep things nice and simple, even an interactive GUI, don’t encourage live questions during a demo, and never change a presentation on the fly.

“The challenge we took on at DAC this year, however, was just the opposite of all of this. We hadn’t seen the design in advance, and it could have been done 10,000 different ways, and absolutely anything could have gone wrong. – overall, a pretty ambitious plan!

“However, Oski Technology has been doing design services since 2005 and we had enough faith in our team to hope that through a live stream of our efforts we would give people a feel for what they have to go through to do formal verification, to bring to life the process of creating a formal testbench from scratch.

“We also wanted to demonstrate the importance of planning to our audience, of taking the appropriate amount of time at the beginning of a project to lay out a strategy of attack. And we certainly succeeded in showing that at DAC. Our efforts clearly would not have been worthwhile without the careful analysis we did at the outset on Sunday night and on into Monday morning.

“In addition, when we receive a project from a real customer, it can come in a variety of forms – in an email, on a wiki, on a phone call, or even laid out on a whiteboard. We also have to deal with files that arrive in a variety of languages, from English to Chinese or Japanese.

“So another of the things we showed at DAC is that with formal verification, no matter the format of the files or the language, you can still piece together a plan and methodology for the formal verification of the design.

“Additionally, we demonstrated in real time that in providing formal verification services, you want to provide a good response to your customer’s design, but you also want to be quick. Good is important, but so is quick.

“We have some customers who put a project schedule in place, and then start dropping features and functionally in order to meet that schedule when they fall behind, or to pull in the schedule. The cost of fixing a mistake in a design later on is high, but does not outweigh the opportunity to get the product to market on schedule. It’s always a tradeoff, and we demonstrated the need for that balance at DAC.

“Most importantly, we met our main goal. We wanted to show that if you only had a formal verification schedule of 72 hours, look at what can be accomplished. It’s true there were quite a few logistical issues, particularly in streaming our progress to the booth, but in the end I’m delighted we did this. And our work is being used by Nvidia. The design we worked on is going into a near term project

“At Oski, we are not building tools, but are building a methodology using existing tools from all the major vendors: Cadence, Synopsys, Mentor, and Jasper. We use these commercially mature tools to run formal verification on complex design problems.

“Anyone with experience in computer science know that model checking has always been hard. But we are expert at building abstraction models that allow us to step out of the box – given a particular design and using a particular set of tools, we can build a fast abstraction models for certain subsets of the design that can achieve astonishing speeds.

“We build the models in Verilog or SystemVerilog and then give the source code to our customers. They can learn from those models, or duplicate them, to further their verification requirements.

“Formal verification is not appropriate for every situation, and it’s important not to apply formal to certain blocks in a design. Also, there are different types of formal verification, so it’s always important to understand the context of what you’re designing. But if the methodology is applied correctly, if it does fit in, formal verification can provide excellent results.

“We succeeded in demonstrating that clearly at DAC. It’s about being creative and thinking outside the box. It’s about accepting the limitations and appropriate place for formal. You have to understand the power of the methodology and the limitations, and you have figure all of that into your verification plan. We succeed in demonstrating all of that clearly at DAC – and were either very brave or very foolish to try!”

**********************

Tags: 72-hour Verification Challenge, DAC 2012, formal verification, NVIDIA, Oski Technology, Vigyan Singhal

This entry was posted on Wednesday, September 12th, 2012 at 6:51 pm. 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.