Intel pushes assertion language as EDA standard <!-- verification -->

Intel pushes assertion language as EDA standard
By Richard Goering, EE Times
November 5, 2001 (10:10 a.m. EST)
URL: http://www.eetimes.com/story/OEG20011102S0125

SAN JOSE, Calif. — Intel Corp. will throw its considerable weight behind the latest EDA standards effort this week, as it recruits Synopsys, Verisity and Co-Design to back the chip giant's ForSpec formal assertion language. But ForSpec faces competition from three other potential standard languages, and skepticism from a few verification tool vendors that think it's too early to standardize a formal language.

As a growing number of EDA vendors offer "semiformal" tools that let engineers verify assertions and complex properties, concern has grown about the emergence of a Tower of Babel of incompatible, proprietary assertion languages. Intel's EDA vendor partnerships come at a critical juncture, because the Accellera standards organization is close to standardizing both a formal assertion language and an assertion library.

Accellera's Verilog Formal Verification (VFV) committee is just a few weeks away from winnowing its list of assertion lan guage candidates from four to two. Candidates include IBM's Sugar, Motorola's CBV, Verisity's "e" and Intel's ForSpec. VFV will go on to select a winner based on the supporting company's willingness to meet Accellera's requirements.

Harry Foster, VFV committee chairman and chief architect at Verplex Systems, said Intel's EDA vendor endorsements will help — but he noted that the other language providers are each lobbying for their own proposals. He said that Intel, IBM and Motorola have similar motivations for pushing their pet assertion languages: a desire to buy external tools that work with the languages these companies already know and use. "There's a lot of politicking," Foster said.

That Intel went through the effort to sign on Synopsys and other vendors to its language indicates how important the company views standardization. "This is the first specific move by Intel to push the [EDA] industry into standardization," said Gary Smith, chief EDA analyst at Gartner Dataquest. "We badly need t o avoid an assertion language war."

With support from Synopsys and the other vendors, Smith predicted, ForSpec will be a "done deal" as a standard.

As part of Intel's agreements with tool vendors, Synopsys will incorporate ForSpec into the OpenVera testbench automation environment; Verisity Design will add the temporal-logic portion of ForSpec to the "e" language; and Co-Design Automation will merge ForSpec temporal constructs into Superlog.

Verification engineers use assertions in both formal model checking and simulation. A simple example of an assertion is a check that a request is always followed by an acknowledge. Simple, precoded assertions are available from the open-source Open Verification Library developed by Verplex Systems. But when engineers want to assemble assertions into complex, temporal properties, a language such as ForSpec is the way to go.

Language war brewing

Concern about the proliferation of assertion langu ages arose at this year's Design Automation Conference (DAC), where many new verification vendors exhibited. "There were more assertion-language-related tools and presentations than I ever anticipated," said consultant Cliff Cummings, writing in John Cooley's DAC trip report. "I think there will be verification language wars for the next few years until a few winners emerge. This is going to make the Verilog-VHDL language wars look like a skirmish."

By working with EDA vendors and Accellera to standardize ForSpec, Intel hopes to "head off" language competition, said Greg Spirakis, vice president of design technology at Intel. "It will make our lives easier in terms of bringing in tools," he said, "and we also believe that over time, formal specs could be a good way to describe IP [intellectual property] blocks."

Spirakis said that ForSpec is "absolutely" applicable outside Intel, where it's been used in the design of both CPUs and chip sets. Inte l donated it to Accellera, he said, so it can be maintained and honed by a standards body. "We also think it's important to have acceptance by major vendors, so it's not just a paper tiger," he said.

Accellera actually has two formal verification language efforts in progress, said Vassilios Gerousis, chairman of Accellera's technical committees. One is the Verilog Formal Verification committee, which is looking to standardize a property language that's independent from Verilog or VHDL. That's the group that's looking at ForSpec, "e," Sugar and CBV.

The second group, an "assertion committee," is looking at assertion language constructs and semantics for the next generation of Verilog, called Verilog-ACE. Verplex has donated Open Verification Library to that effort.

Accellera's Foster noted that ForSpec, CBV and "e" are all "linear-time logic" languages based on linear sequences of events. IBM's Sugar is a "branching-time logic" language that can branch to in finite possibilities at any point in time. Compared with Motorola's CBV, Foster said, ForSpec has features that make it easier to express extremely complex sequences of events.

Synopsys will add the complete ForSpec language to OpenVera version 2.0 in the first half of 2002, said Farhad Hyatt, vice president of marketing for verification at Synopsys. Although OpenVera itself has an assertion language, ForSpec adds a number of temporal-logic features. Also, ForSpec's assume-guarantee feature supports hierarchical proofs, he said.

"We need to put our energy into better tools and flows, not separate languages," said Rich Goldman, vice president for strategic-market development at Synopsys. "If you ask whether we think ForSpec is a good language to be the standard, the answer is yes. We are going to work to help assure that it is."

Co-Design Automation is working with Intel to integrate ForSpec's temporal-logic functionality directly into Superlog, said Dave Kelf, Co-Design vice president of marketin g. But Co-Design isn't just taking ForSpec syntax as is, he noted. "At the moment [ForSpec] is very hard to use as a language. Building it into Superlog makes it much more efficient," Kelf said.

Competitive standard

While both Goldman and Kelf see ForSpec as a language with industry-wide appeal and applicability, Verisity is not so sure. "Our motivation is really to support Intel," said Francine Ferguson, Verisity's vice president of worldwide marketing. "We have also donated the temporal subset of 'e' to Accellera, so in that sense I suppose it's a competitive standard."

Nonetheless, Ferguson said, ForSpec does have some model-checking operators that are not found in the "e" language. Verisity will thus expand the "e" language to include the temporal subset of ForSpec.

Verplex has diverged from Intel's approach by providing not a new language, but an assertion library built on top of Verilog. Dino Caporossi, vice president of marketing at Verplex, said the Open Verification Librar y assertions are sufficient for the kind of checking most designers will want to do. But for verification engineers who want to look at complicated sequences of operations, he said, an assertion language such as ForSpec may be the answer.

"Our R&D group has found ForSpec to be a strong language," Caporossi said. "It has a good compromise between ease of use and functionality. It uses linear temporal logic, which is more intuitive to engineers [who are] used to a simulation-based methodology. Multiple clock and reset signals make it even more flexible."

Shaky certainty

Many smaller verification vendors, however, are less sure about the direction of formal-language standardization.

"Real Intent believes that instead of defining a new specification language, the correct and more adoptable approach is for the standard to leverage the existing framework of Verilog and VHDL," said Prakash Narain, Real Intent's president and chief executive officer. His company is participating in Accell era's assertion committee.

But 0-In Design Automation appears to be taking the opposite view. That company is helping select a language as part of Accellera's VFV committee, but believes efforts to standardize an assertion library are "premature," said Tom Anderson, vice president of applications engineering at 0-In.

Averant, for its part, is "encouraged" that Accellera is working to standardize an assertion language, but isn't ready to support the effort, said Behrooz Zahiri, Averant's vice president of marketing.

"We are concerned that at this time, the industry collectively does not have sufficient real-world experience to design and freeze a standard language," Zahiri said. "We are also reluctant to contribute what we have paid a high price to learn."

Verification startup @HDL, meanwhile, will support whatever standard Accellera comes up with, but has some concerns, said Richard Curtin, @HDL's chief operating officer. The challenge, according to Curtin, is to come up with something that can be widely used by people other than "specialists" at Intel, Motorola or IBM.

"A lot of these model-checking companies are trying to do their own thing," noted Co-Design's Kelf. "Some companies see tools as their differentiator, but others are seeing the way they specify properties as a differentiator. They're nervous in getting involved in that [standardization]. Once we break that, we'll be in good shape."