Oski Technology: Bullish on Formal Verification

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.

Vigyan Singhal is Oski Technology’s founder, president and CEO

Vigyan and Oski Technology may seem synonymous to anyone familiar with the company, though he demurs at that portrayal and points to the formal verification services company’s 25 employees in the U.S., India and China. Yes, he started the consulting business in 2005, but that’s only a small part of the story.

Let’s start, then, with Vigyan’s story and move it forward. Vigyan’s from Northern India and studied at the Indian Institute of Technology (IIT, as it’s known) Kanpur, the prestigious and hard-to-get-into college in India. After completing his Bachelor of Science degree in computer science and engineering at IIT Kanpur, he was accepted at Cal and started working toward a Master of Science degree and Ph.D. in database systems. He was not making much progress even after three years and was discouraged. After repeated cajoling from a friend, he finally agreed to take a course with Dr. Robert Brayton, the Cadence Distinguished Professor of Electrical Engineering and Computer Science and a Phil Kaufman Award recipient.

Soon after, he switched majors and was part of Professor Brayton’s group. Right after inducting Vigyan in his group, Professor Brayton got him an internship working at Motorola in Austin, Texas. His supervisor was Carl Pixley, now of Synopsys, who asked him to do research on formal verification techniques, which later would evolve into his thesis topic. Carl also asked him to verify the cache controller in a PowerPC chip, where Vigyan found his first post-silicon bug using formal verification.

When his doctoral studies were wrapping up, he was assigned a dream-team thesis committee if there ever was one. Along with Professor Brayton, he presented to Dr. Alberto Sangiovanni-Vincentelli and the late Dr. Richard Newton. A funny thing happened during his qualifying examination presentation for his thesis topic. Professor Newton stopped him and said that the formal verification methodology he was outlining wouldn’t work. Professor Sangiovanni-Vincentelli jumped in, arguing Vigyan’s points. Vigyan and Professor Brayton went back to Brayton office to talk it through. He went on to get his Ph.D., with a thesis in the methodology he proposed.

With the newly minted degree, Vigyan joined Cadence Berkeley Labs and began developing what would become Cadence’s formal verification entry HECK, an equivalence checking tool. Vigyan stayed around for about 18 months after his project was commercialized, then partnered with another Cadence engineer, Joe Higgins, originally from the analog/mixed-signal group, to launch a verification company. They called their fledgling startup Tempus Fugit, Latin for “time flies.” Vigyan and Joe looked at areas within the formal verification discipline, bootstrapping themselves with consulting services projects. Their customers’ designs became their inspiration.

“I was inspired by the designs I saw at Apple,” says Vigyan. He and Joe began developing model checking software to verify the correctness of standard interfaces, such as PCI, USB or FireWire. Even though there were nine other commercial tools in formal verification market from 0-In, Averant, Axiom, Cadence, Chrysalis, Real Intent, Synopsys, Verplex and Verysys at that time, Vigyan and Joe believed they could build a differentiated company. Within three months from the start of product development, they had their verification engines and attracted early customers Ikanos and NVIDIA.

Vigyan persuaded both with the convincing offer: “Let me use my tool on your design and pay me if I find bugs.” He succeeded at both companies by finding important bugs.

Rahul Joshi, Oski Technology’s managing director of India Operations

For those EDACafe readers who don’t recognize the name Tempus Fugit, it’s been renamed as Jasper Design Automation, a well-respected verification provider, since 2003. About two years later, and after an influx of capital and the appointment of Kathryn Kranen to the role of CEO, Vigyan left to form Oski Technology.

Here’s where the discussion turns fully to Oski Technology, a company that’s been growing steadily since 2005. To support the growth of formal adoption in semiconductor companies, Oski quietly acquired a company in New Delhi, India, comprised of talented and clever engineers, almost all of whom are IIT graduates, led by Rahul Joshi.

“They brought with them new ideas and concepts,” remarks Vigyan, who’s building a core group of engineers to offer formal verification services, along with training programs to teach chip verification engineers how to build test cases.

Additionally, Jin Zhang has been hired to serve as general manager for Asia Pacific to support demand for formal verification services and manage the distribution channel in this region. Jin holds a Ph.D. in formal verification and a MBA in international management, and has held technical and management positions with increasing responsibilities at EVE, Real Intent, Cadence Design Systems and Lattice Semiconductor.

Jin Zhang, general manager of Asia Pacific and senior director of marketing.

Today, Oski is focusing on the tip of the pyramid of all formal applications –– or what it refers to as End-to-End Formal. The goal is formidable because it means catching bugs early, increasing verification efficiency, replacing block-level simulation and enabling formal verification sign-off. A heady goal, to be sure, but one Oski’s managing with aplomb.

When the Oski team of formal verification experts is deployed on a chip design, it uses an internal Formal Sign-off Methodology to find the most elusive bugs. That methodology includes end-to-end checkers, Abstraction Models and formal coverage. Oski’s verification engineers have developed formal verification IP that’s licensed and sold to their customers, but Vigyan makes it clear that Oski is a formal verification services company and not a tools supplier.

A rule of thumb from the early days of Tempest Fugit is employed again today, Vigyan notes with pride: “Formal is unpredictable and we’re paid only if it works.”

He quickly adds: “We know so much about formal verification and how to make it tractable.”

Oski is bullish on expanding the understanding of the pyramid so verification engineers can implement End-to-End formal technologies and methodologies to accomplish their verification goals.

Formal Verification includes a range of technologies, he remarks as he points to a pyramid on his computer screen (see above). Oski is bullish on expanding the understanding of the pyramid so verification engineers can implement End-to-End formal technologies and methodologies to accomplish their verification goals to the point that they can sign-off on certain blocks using formal alone. Currently, the awareness and understanding is at the bottom of the pyramid and Oski’s often called into a chip design and verification project to solve the hardest problem at the tip of the pyramid.

Expanding the pyramid is more easily typed than done. “We have few teachers, so few people know how formal verification works,” remarks Vigyan, shaking his head sadly. “It’s not taught at universities and tool providers are supplying apps that automate tools.”

This unfortunate state was another inspiration for Vigyan and Oski Technology, which unveiled the Oski Deep Formal Award last year at the Formal Methods in Computer-Aided Design (FMCAD) Conference. In doing so, Oski became the first industrial sponsor of the annual Hardware Model Checking Competition (HWMCC).

The award, to be given again this year during FMCAD in Portland, Ore., in October, is designed to encourage research for developing tools and making formal verification more practical. “Our hope is that cool ideas will make its way into tools,” he says. The second reason is to help advances in bounded model checking. Currently, model checking results often appear inconclusive. For the experts at Oski Technology, unbounded proofs are useful and rather reliable, but it is not a well-understood concept.

Oski Live Verification Challenge at DAC 2012

On a lighter note, Oski Technology is more than committed to formal verification. It lives it. It’s hard to forget Oski’s show-stealing feat at DAC 2012 in San Francisco with its 72-hour verification challenge. An engineer, Chirag Agarwal, was holed up in a conference room close to the Moscone Center and tasked with debugging an NVIDIA design with Oski’s Formal Sign-Off Methodology in 72 hours, on a design he had never seen before. Nor had anyone else at Oski.

A CCTV was installed in the conference room and the video was streamed live in the Oski booth. Talk about a nail biter! Even Vigyan will admit that there were a few tense moments on the first day of DAC, but then they knew they had pulled it off. The NVIDIA team received detailed verification results delivered at 5 p.m. Wednesday as DAC was closing, including the end-to-end formal testbench, and three formerly undetected corner-case bugs.

This year’s DAC was a bit more subdued, but no less creative and bullish on formal verification. Oski offered a verification test challenge each day. Attendees who walked up to the booth were given a problem to solve and awarded great prizes for the correct answer.

Winners of Oski’s DAC verification challenge this year received a beer stein.

If that’s not all, the wildly inventive Oski Technology team is at it again. It formed the Oski “Decoding Formal” Club to foster formal idea sharing among formal verification enthusiasts and proselytize formal verification. The first invitation-only meeting will be held at the Computer History Museum in Mountain View on October 10.

As the discussion with Vigyan comes to a close, it’s clear that while the Oski Technology mascot may be a bear and its founder inspired by Cal, Oski Technology is quite bullish on formal verification.

(Editor’s Note: Nanette Collins manages Oski Technologies’ Public Relations activities.)

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

Category: Articles

This entry was posted on Wednesday, October 2nd, 2013 at 6:28 am. 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.