Oski Technology: Establishing the Decoding Formal Club

If you are someone who does formal verification and is looking for a chance to talk over the challenges with others who do similar work, Oski Technology has something that may be of interest to you. Starting this month in Silicon Valley, the company is kicking off its Oski Decoding Formal Club. The inaugural meeting took place at the Computer History Museum on October 10th, and was lead by company CEO Vigyan Singhal.

Over lunch, he presented a 45-minute overview titled, “Using Bounded Proofs in Formal Sign-off.” Singhal noted during his talk that it’s the reality today that formal is expensive and returns “low bang for the bucks.” He insisted, however, that if there were places to learn more about how to apply formal verification, and how to build a productive formal team, the technology would be more widely applied and its destiny more quickly fulfilled as an extremely effective technique for use end-to-end throughout the design process.

Following Singhal’s presentation, the 20+ people in attendance (representing 10 companies) were each given time in a relaxed, roundtable environment to share their experiences and/or frustrations with formal. The companies included Apple, Broadcom, Cisco, HiSilicon, Memoir Systems, Microsoft, Nvidia, Palo Alto Networks, Qualcomm, and a startup. In other words, companies both big and small were represented and the resulting conversation was very interesting. It was clear as the talking stick was handed around, that some practitioners were very confident and sure of themselves, while others were relieved to know they’re not the only ones who struggle with formal.

Oski Technology’s obvious motivation for establishing the club and hosting regular meetings going forward is outreach to their customers. Oski’s a consulting firm and believes, per Vigyan Singhal, that “formal is powerful, but needs expertise. Yet few companies have the critical mass or know-how to use formal effectively.”

The motivation for those attending the kick-off meeting of the Formal Club was not as obvious, given that some people didn’t seem to have problems. No matter the level of confidence, however, the 90-minute roundtable discussion revealed a lot of differences of opinions, not just about the effectiveness of formal, but also about where to place the blame for slow adoption in the industry.

Some speakers were certain the problem lies with management: Management doesn’t see the benefit, so is unwilling to fund the necessary training and deal with the growing pains associated with implementation.

Other speakers were adamant that it’s more a problem of methodology: How to integrate the use of formal in and around simulation, and at what level in the design. Formal, per several speakers, is very useful at the block level, but not at a higher level after the blocks have been integrated into a system. Even knowing how to define the appropriate block for formal, according to some in the room, is not always obvious.

Then there are problems with the design team. Multiple speakers in the room on October 10th felt that designers are frequently oblivious to the needs of verification and blithely make changes mid-project – introducing a cycle delay in a block interface, for instance – without paying the slightest attention to how that might invalidate checkers already in place.

At least one speaker in the room advocated, therefore, for embedding the verification team within the design team so an ongoing conversation can take place throughout the course of the project. Problems are handled as they come up, and not after the fact when errors precipitate a nasty blame game between design and verification as to who’s responsible for a failure.

Finally, many spoke about the problem of legacy skills as an impediment to adopting formal: “For people who have been doing simulation for years, it’s hard for them to switch to formal.”

As the 90-minute roundtable session wrapped up, Singhal called the first meeting of the Oski Decoding Formal Club to a close. He asked those who would be interested in participating in ongoing sessions such as this to let him know.

Clearly not everyone who was in the room is going to sign up, but given the challenges laid out by the group – issues with management, conflicts between design and verification teams, problems of getting engineers to embrace new methodologies, and complex technical questions about how and when to apply formal – there’s certainly enough on the table to create a set of sessions centering on each of these topics, and more, for those who are interested.

Those who have something to learn, and a willingness to share that with others, have a great opportunity here and should take advantage of Oski Technology’s willingness to establish and maintain the Decoding Formal Club. Promoting the good that formal can do, and widening its user base, should be an obvious outcome of such an effort.

*******************
Mission Statement …

“The Oski Decoding Formal Club is a forum for formal enthusiasts, pioneers, leaders and friends who work to promote the sharing of ideas, the advance of formal technology, and the adoption of formal sign-off within the industry.”

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

Tags: Oski Decoding Formal Club, Oski Technology, Vigyan Singhal

This entry was posted on Thursday, October 24th, 2013 at 10:21 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.