Oski Technology: Formal celebrates its Place at the Table

Since initiating their Decoding Formal Club in October 2013, Oski Technology has hosted this much-needed get-together every quarter, most recently on October 21st of this year at the Computer History Museum in Mountain View. I was fortunate to attend the debut meeting in 2013, so it was interesting to hear from Oski VP Jin Zhang that the support group is proving valuable to the growing numbers who attend.

“The first time we held the meeting,” Zhang said, “it was by invitation only, and we included about a dozen folks. Since that first event, we have continued to use the same room at the Computer History Museum, a room that can hold up to 40 people.

“The workshop, however, is continuing to grow very nicely, so we are faced with either finding a new venue or working with the museum to arrange for a bigger room for our next meeting in the first quarter of 2016.”

Zhang said interest in the event has increased to the point that people sign up to attend as soon as the date and time are announced. “They want to be sure they’ve got a spot,” she said.

I remembered that Apple was a surprising attendee at the original meeting in 2013; Zhang said they are still participating: “Yes, and many names in the industry that you know well continue to attend. Larger companies such as Apple, Google, and Intel, and smaller companies as well – a range of companies representing all levels of expertise in formal verification.

“Everyone in attendance, whether they’re new to formal or moving to it as a career choice, wants to offer something to [the group], because they know they can benefit from the discussion.”

Still, I said, it seems surprising that these larger, famously secretive companies attend so openly.

Zhang replied, “Oski is in the formal verification services business and we do not mind sharing our knowledge with the whole industry, including companies who are not our customers – even if they are secretive. We do regularly ask them to participate as speakers, and they continue to decline, but it is our hope that someday they will change their minds and present to the group.

“Meanwhile, other companies are very forthcoming at our meetings. Companies like NVIDIA, ARM, and Broadcom all presented in October, and were very enthusiastic. They agree with us that the industry can only grow when people share what they know with each other.

“At Oski, we continue to be very hopeful that even more people will come forward and share their experiences as the quarterly meeting continues to grow in importance.”

I asked Zhang what needs to change for companies like Google and Apple to participate as presenters.

She said, “It is clear that engineers from these companies need to get management’s permission to speak, but even then we would not expect them to [reveal too much until]. Hopefully, their upper management will eventually recognize this participation has value and agree to it.

“[The truth is], we don’t really want to know the details of their designs. What the audience wants to learn about are techniques related to formal, things which would be helpful in their own work.

“We believe that with time even the [secretive] companies will see that their engineers would benefit from sharing their experiences with the community and will allow them to contribute to growth in the formal community.”

Two years into their work hosting the Decoding Formal Club, I asked Zhang if Oski has learned anything surprising along the way.

Her answer was simple: “Just the amount of interest from people working in formal technology itself.

“We obviously see that level of interest [reflected in] our business growing so well, and are pleased that formal is finally getting the place it deserves in the verification space. But the growth of the Decoding Formal Club, and the increasing numbers of people interested in learning about formal, has surprised us.

“I have been doing formal for almost 20 years and I know how difficult it was in the early years. But now we have a lot of interest in the technology, that’s just how fast things are changing.

“We are now getting many requests to take our event to other areas, everywhere from Austin to locations in China and elsewhere in Asia. Today companies everywhere are recognizing the value of formal and are [working to increase the knowledge of their engineers].”

“Another development we are seeing,” Zhang added, “is a great shortage in formal expertise in the industry.

“People who [understand this technology] are now getting very good compensation, and engineers are seeing this as a great career choice – so much so, that some of the newer engineers are choosing formal as a career path rather than traditional verification.

“Many companies are looking to hire engineers with this expertise, or trying to grow their internal teams to increase [their formal capabilities]. They are also working with us to help train their [existing teams] in our methodology around formal.

“Worldwide today, however, the whole formal industry is less than 200 people. That is a very small community and one of the reasons why we started our club.”

I asked if traditional verification engineers are too far down the path to retrain in formal methods?

“Yes,” Zhang replied, “but traditional verification is always needed. And even though we know formal will replace simulation at some level, there will always be a role and place for traditional verification.

“Still, learning formal is very different. It’s actually orthogonal to simulation and easier for someone with a fresh point of view to learn, rather than trying to convert someone with years of traditional verification experience.

“Today, we see engineers from many different disciplines – electrical engineering, mechanical engineering, and computer science – going specifically into formal at the beginning of their careers.”

Is it because the tools have improved that formal is no longer strictly the handiwork of PhDs?

She said, “Yes, the technology has improved. Previously, formal verification could only be applied to small blocks in a design, but now we’re doing formal on complete blocks.

“Even today, however, for complex blocks you still need a lot of manual effort. It’s not yet push-button, so if someone has a PhD in formal it can help, it can be easier to understand some of the techniques being used daily.

“But a PhD is no longer absolutely necessary, because engineers can learn a lot of the techniques we’re using even without understanding the algorithms [inside of the tools].”

Zhang added a caveat to her suggestions that formal is now available to a larger pool of engineers, distinguishing between layers of formal:

“The bottom layer in the formal pyramid is automatic checking, an area where Cadence, Synopsys, and Mentor all provide tools that automatically extract certain properties.

“At Oski, we don’t have a preference for the tools of one vendor over another. We’ve used them all, and believe they’re wonderful. We can make them all work and see ourselves as equal partners with these vendors.

“Nonetheless, this layer of formal is a simplified-use model and has its limitations because it provides less information.

“The next layer of formal is more complex, and is about a particular problem – clock-domain crossing, low power, connectivity – formal suites of apps that don’t solve all problems, but are important, and a little harder than automatic formal to apply.

“The third layer up is where you have to write assertions in RTL in order to find bugs. This is useful for finding problems in the design, and has been used for standard model checking.

“The fourth and top layer is end-to-end formal. If you think of a chip as a unit, what we [are looking at] is from the input to the output of the chip. The properties we write are on the output of the signal and only use the input signal [for checking], where assertions are embedded properties and involve finer internal granularity.

“Writing an end-to-end checker takes a lot of expertise, and is something that we specialize in at Oski Technology. This layer and the previous two layers are [more appropriate for] engineers with the level of expertise associated with a PhD.”

Zhang said that is why Oski has such an important role in the industry: “Even with advancements in the tools, it is the methodology that is critical. And that requires a much higher level of expertise.

“We are providing that methodology, and allowing our customers to now use formal to sign off-on on really complex designs. We [are giving them the confidence to know] that there is no bug in this block or that, something simulation can never guarantee.”

“In the early days, you couldn’t use formal for sign-off. But now,” she concluded, “with methodologies like ours and good tools from the vendors, more and more companies are recognizing formal as a must-have technology. Something that should have a rightful place in verification and complements simulation very nicely.”

*****************
Also very nice …

The October 21st meeting at the Computer History Museum included a cake to celebrate Oski Technology’s 10th Anniversary in business and the 2nd Anniversary of the Decoding Formal Club.

“It was very cool,” Zhang said with enthusiasm.

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

Tags: Apple, ARM, Broadcom, Cadence, Decoding Formal Club, formal verification, Google, Intel, Jin Zhang, Mentor Graphics, NVIDIA, Oski Technology, Synopsys

This entry was posted on Thursday, November 5th, 2015 at 8:35 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.