RTL Verification

Oski Challenge Success: Oski Verifies NVIDIA Design Live, in 72 Hours

Some said it couldn’t be done, but the Oski Technology team set out to prove it was possible to take a new design sight unseen, and formally verify it in 72 hours, live and on camera at DAC 2012 during the Oski Live Verification Challenge. What makes this feat even more impressive is that not only did Oski build a new formal testbench from scratch in 72 hours, they also found three bugs since confirmed to have been missed with simulation thus far. See below for an update on the Challenge and the newly released Oski Challenge Video.

NVIDIA & Oski Success: Live Formal Verification Challenge

The chosen submission was a live design from NVIDIA, whose engineers were doubtful at the outset about the feasibility of the Challenge. “I was convinced of some success,” said Dan Smith, Senior Director of CAD and Methodology “but in 3 days, with a new design that has not been seen before, a very complex design – [I was] skeptical, to say the least.”

The Oski Live Verification Challenge was indeed an unprecedented victory for Oski. “The Oski Challenge was about demonstrating how effective formal testbenches for complex designs can be built in a short time using formal testplanning” says Oski Technology CEO Vigyan Singhal.

Singhal explains, “Additionally, we hoped to show how the Oski experts can deliver results by applying formal verification based on limited information and little or no designer interaction, and within extremely tight deadlines.”

Formal: A Widening Array of Possibilities

A more important dimension of the Challenge says Singhal was to demonstrate the value of Oski’s unique Formal Verification Methodology and approach wherein a comprehensive plan was crafted early on in the process, positioning Oski to be successful. A carefully created strategy was especially critical given the extremely difficult conditions of the Challenge, including public scrutiny and very real and rigid time constraints.

The Challenge also presented a widening array of possibilities offered by the strategic deployment of formal verification using the Oski Plan-Verify-Measure methodology; Oski engineers built end-to-end checkers during the Challenge, and found four corner-case bugs in the process.

Preparing for the Challenge: A Week Before DAC

With just one week to go before DAC, five customers had confirmed interest in participating in the Challenge. After some discussion, a design from NVIDIA was selected. NVIDIA prepared a tarball including the RTL of the design, two example simulation waves, and a document for the functional specification of the design. The tarball was then encrypted by NVIDIA and submitted to Oski. The design was a module on the ARM AMBA AXI interface, to be used in an upcoming chip for the NVIDIA products. Oski was provided two pieces of information in advance: first that the design was implemented by two designers, and second that it had been verified with simulation but had not yet taped out. The actual design and documentation were encrypted with an OpenSSL key, known only to NVIDIA until the official start of the Challenge at 17h00 on Sunday.

The Oski Challenge office space was set up within a few blocks of the Moscone center in downtown San Francisco. A live video stream, Twitter feed and the Challenge countdown clock captured the action live on LCD screens at the Oski booth and via a public video stream on the Oski Challenge page on the Oski Technology web site, starting with the Challenge kickoff at 17h00 on Sunday. Cadence Design Systems provided Oski Technology with licenses for Incisive Enterprise Verifier (IEV) for use during the Challenge.

Oski Live Verification Challenge: Sunday, Day 1

Sunday, Day 1 at 17h00: NVIDIA handed off the decryption key to Oski at the Challenge kickoff. The Oski Challenge team accessed the RTL files, documentation and the simulation waves, and the NVIDIA team left. One of the first things the Oski engineers did was compile the design to check for completeness. An hour and a half later, the Oski engineers discovered that the module definitions of 8 different library modules, including a clock gater, synchronizer, and others were missing.

Without after-hours access to the designers, retrieving the missing files from NVIDIA was not an option. Instead the simulation waves and module names were used to guess at the functionality of these modules, and then the Verilog for these modules was written by hand. Writing such Verilog in a short time-frame is no trivial task, but without access to input from the designers, this step was necessary in order to move to the next stage.

After a quick read of the 20-page specification, the Oski engineers decided to focus exclusively on verifying the Read path during the 72-hour Challenge, and leave the verification of the Write path for a later date.

Formal and the ARM AMBA AXI Interface

One side of the design was the well-known ARM AMBA AXI interface, the other was a proprietary interface that the team estimated would take a few hours of work to model. The design had two interacting Read and Write paths, with sufficient amount of re-ordering of address and data beats, that could introduce worrisome corner-cases. There were RTL assertions in the design, although these were inside a define that needed to be exposed to the formal tool. Additionally, the engineers had to write the Verilog for the assertion modules, since these were not included in the tarball. Next, they wrote some simple covers on design outputs, and soon discovered these were failing. The problem seemed due to some faulty reset modeling, but it was time to call it a night.

Oski Live Verification Challenge: Monday, Day 2

The first task was to prioritize the list of constraints and checkers to write for the day. Monday, Day 2 was all about being in the trenches. The engineers had to work out a lot of issues, and made mistakes in the testbench. They started off by trying to model the two different clocks in the design, and constraints to ensure inputs did not toggle more often than needed. Next they wrote some basic constraints on the interfaces, and added their first checker. A large part of the day was iterating through false failures, and adding design-specific constraints, as needed. This is a necessary process for any formal testbench. To avoid proof complexity, they intentionally did not add all known constraints from the beginning, and instead added these only as needed. This included adding constraints for the ARM AMBA AXI interface.

By midday on Monday the Oski engineers were wondering if this process of constraint iteration was going to converge in time. With just 48 hours to go, were the team’s efforts going to produce anything interesting or useful?

Back at the Oski booth on the DAC floor, there was enthusiasm, interest, excitement – and a touch of skepticism – from customers and prospects as they tracked the progress of the Challenge.

By the end of the day, things were looking promising: The Oski engineers were able to get some intriguing counterexamples that indicated that they may be close to seeing real or interesting traces.

Oski Live Verification Challenge: Tuesday, Day 3

Tuesday, Day 3 started off well, and things seemed to be back on track. The first few counterexamples were eventually root-caused to some missing constraints relating inputs on different clock domains. The engineers used the customer-provided example simulation waves, to further their understanding about what was legal on the interfaces. By midday Tuesday the team had found a more realistic counter example. It looked like a real problem. They went into a debug phase and root-caused it to a specific line in the RTL. Better yet, when the Oski team changed the RTL to what they thought the fix was, the end-to-end checker started passing. At 15h15 Tuesday Oski tweeted the confirmation that this was a real bug. From there on out, things were golden. They attempted to prove a second end-to-end checker and found another bug by the end of the day. It was an exhilarating moment, and a thrilling end to the day.

Booth visitors were invited to submit questions directly to Oski engineers via Twitter, and one booth visitor submitted a question live by phone and on camera.

Oski Live Verification Challenge: Wednesday, Day 4

On Wednesday, the last day of the Challenge, the Oski engineers had a couple of options. They could go on and verify the Write path, but decided instead to try out something different and ambitious: Build an X-propogation app from scratch to prove the design does not produce X’s under any corner cases situations. The X-propagation app works by making two copies of the design, and comparing the outputs of the two designs — if an X can propagate to an output, it will show up a mismatch. Sure enough, by noon on Wednesday they found a corner-case bug which would get triggered only when a counter under-flowed, and caused an array indexing bug, under corner-case conditions. Later in the day, they found a second X-propagation bug where a control flop was not initialized at reset. Once the RTL was changed to initialize this flow, this check passed.

To wrap up the day on Wednesday, the Oski Challenge team tidied up the testbench, created a README file and a tarball for the customer, complete with traces for the failure. The Oski Live Verification Challenge proves that formal verification can be very effectively deployed on a new design and in a short amount of time, something that cannot be done with simulation today.

Oski engineers credit the systematic application of formal within the Oski Plan-Verify-Measure methodology for their enormous success in such a compressed time frame.

Oski Live Verification Challenge: Post-DAC Review

In the week following the Challenge, Oski delivered a detailed on-site review at NVIDIA of the testbench and the bugs found. Three of the four bugs found were confirmed to have been thus far real misses with simulation. The fourth bug was due to a class of disallowed AXI transactions that was not listed in the specification.

Soon after the detailed report was delivered, the verification plans for the design were altered to incorporate more formal verification and address the areas covered during this challenge, and NVIDIA staff are strongly optimistic about the future application of formal verification on similar designs.

Shankar Govindaraju, platform architect at NVIDIA explains. “If you can verify something [in a lot shorter] time, that has got a lot of value; it has got a lot of bang for the buck.”

Says Anshu Nadkarni, Director HW Engineering, “End-to-end verification is extremely valuable for NVIDIA. With very tight deadlines and aggressive schedules, it is extremely difficult to come up with a comprehensive verification plan without actually understanding the micro-architecture.”

Nadkarni adds that the results of the Challenge exceeded his expectations. “It is a testament to the skill of the verification engineers, and pretty phenomenal what they were able to achieve.” Smith too was impressed: “I thought the Oski challenge was a really great idea. It showcases what the Oski company is about, the services they provide and the successes they [have had].”

Challenge Success Showcases Formal in Real Time

Says Oski CEO Vigyan Singhal, “The Oski Live Verification Challenge was not only an opportunity to showcase what could be done with formal on an extremely tight deadline, but have that success extend beyond DAC, in a real customer setting.”

Oski’s formal verification methodology has added value to a real design that is slated for use in mobile devices that will be on store shelves in the future.