Synopsys, Intel push OpenVera 2.0 assertion language

Synopsys, Intel push OpenVera 2.0 assertion language
MOUNTAIN VIEW, Calif. — Synopsys Inc. and Intel Corp. this week will pitch yet another new candidate for an industry-standard assertion language: OpenVera 2.0, which includes Intel's ForSpec property language. But the companies appear to be heading for a showdown with the Accellera standards organization, which is pursuing three of its own initiatives and which recently rejected ForSpec.

All of these efforts are aimed at heading off a Babel of proprietary assertion languages. Such languages, which let engineers check properties during simulation and formal verification, have become crucial for complex chip design.

However, competing and overlapping standards efforts threaten to cause as much confusion as the proliferation of proprietary formats itself.

OpenVera 1.0, an open-source verification language managed by Synopsys, already had an assertion capability for simulation. With the addition of ForSpec, OpenVera 2.0 supports formal tools as well, and the move has garnered support from design-tool vendors @HDL, Novas and Verplex.

"The whole concept is to have one language that supports both simulation and formal verification," said Steve Meier, group R&D director for formal verification at Synopsys. "It's important because designers want a single engine and one golden specification."

ForSpec today, however, is a formal-property language used primarily by systems architects. It's unclear to what extent register-transfer-level designers will use its capabilities. The Superlog Design Assertion Subset (DAS), recently donated to Accellera by Co-Design Automation Inc. and Real Intent Corp., aims more squarely at RTL designers by proposing to add an assertion construct to Verilog.

In addition to the DAS, Accellera's System Verilog committee is also working to standardize the Verplex Open Verification Library of Verilog assertions. And Accellera's Verilog Formal Verification (VFV) committee, looking to standardize an HDL-independent formal-property language, recently rejected ForSpec and is down to two candidates: IBM's Sugar and Motorola's CBV.

As it has in the past, Synopsys maintains that a vendor-managed open-source effort is a surer path to an industry standard than a broad standards body.

"I don't think there's a collision course between OpenVera and the Accellera VFV, but we are well ahead of where the VFV will be," said Rich Goldman, Synopsys' vice president for strategic market development. "As Accellera moves through their mechanism, we will continue to be very far ahead."

Accellera chairman Dennis Brophy responded that Accellera's wide representation among semiconductor and electronic-design-automation companies can best facilitate standards. "I think when we have a broader level of participation, it's going to assure a higher level of adoption vs. an EDA-company-only proposal," he said.

"Obviously Synopsys and Intel have the capability to drive this standard," said Gary Smith, chief EDA analyst at Gartner Dataquest. "Synopsys is now one of two formal-verification vendors who count, and Intel has more formal-verification engineers than the rest of the world combined. Just as obviously, they are competing with Accellera's formal-assertion standard committees."

Going formal

Assertions allow designers to check properties, such as sequences of events that should occur in a given order. ForSpec provides syntax that lets designers describe complex sequences and clocking styles, and employ asynchronous resets.

But the main additions to the previous version of Vera are new constructs and operators that support formal tools. In addition to formal operators, Synopsys' Meier said, ForSpec brings directives such as "assume," "restrict," "model" and "assert" that are aimed at formal tools. An "assume-guarantee" construct lets assertions used as module-level properties become monitors at higher levels of hierarchy.

The entire "public" version of ForSpec is contained within OpenVera 2.0, said Greg Spirakis, director of design technology for Intel's architecture group. "In-house, there will always be some minor tweaks," he said, but otherwise the announcement means ForSpec is now in the public domain and is no longer under Intel's control.

Spirakis said Accellera's VFV rejected ForSpec because "it was not part of a faction looked favorably upon. I don't believe it had any technical weakness." Synopsys' Goldman was more blunt, calling the ForSpec rejection the result of "politicking."

Not so, said Accellera's Brophy, who insisted the selection process was based on adherence to Accellera's requirements. In fact, he said, none of the submissions met all of the VFV committee's requirements, so whatever emerges as a standards proposal will represent a modification of an existing language. Brophy said Accellera hopes to have a specific proposal by this June's Design Automation Conference.

Competing standards are "certainly a possibility," Intel's Spirakis acknowledged. "We have stayed members of Accellera even though our technology was not selected. We are working with them to modify their final version to be compatible with ForSpec. The jury is out on whether that will happen or not."

Spirakis also said that Intel, an investor in Co-Design, wants to "reconcile" any overlap between the Superlog DAS and ForSpec. "We don't know yet whether that will be possible," he said.

While ForSpec is used primarily by architects within Intel, there's no reason it can't be used by RTL designers, Spirakis said. Synopsys' Meier concurred. "We think that one language can pretty much meet the entire market's needs." Meier said, however, that he expects most RTL designers will use a "small subset" of the OpenVera 2.0 assertions, or instantiate prebuilt assertions from a library. Above RTL, he noted, OpenVera 2.0 can be used to write protocol checks at the boundaries of blocks.

Tool support

OpenVera 2.0 won't get far without EDA tool support, and thus far, there are three endorsements. @HDL Inc. this week will announce that it will support OpenVera 2.0 assertions with a bidirectional interface to its @Verifier and @Designer verification products. The interface is set for release in June. "With the industry experience that Intel has had over the years of using ForSpec, there is already a proven methodology and technology," said chief operating officer Richard Curtin.

Novas Software Inc., which has already announced its support of the Superlog DAS, will link OpenVera 2.0 to its debugging software, but has no firm timetable. "We'll support both initiatives because we believe an open assertion capability is vital," said Scott Sandler, Novas' president and chief executive. "I don't have any preference for syntax."

Also endorsing both the Superlog DAS and OpenVera 2.0 is Verplex Systems Inc., which will support OpenVera assertions with its BlackTie formal-property checking tool, said K.C. Chen, chief technology officer at Verplex.

Forte Design Systems last week said that its Perspective verification-results analysis product will support OpenVera, although the announcement was not specific to OpenVera 2.0.

Synopsys this week will also announce 11 new members of the OpenVera Catalyst program, which provides verification intellectual property — reusable modules that typically include bus-functional models, traffic generators, protocol monitors and functional-coverage blocks.

Open standard

Synopsys' Goldman noted that OpenVera 2.0 is an open-source language that anybody can license, and to which anyone can contribute. "All you have to do is click and download it," he said.

Synopsys, however, controls the "main fork" of OpenVera. Anyone can change it and write a new fork, but Synopsys expects that the vast majority of users will stick with OpenVera as defined in the Language Reference Manual, available at the OpenVera Web site.

Goldman maintained that OpenVera today has "much stronger support" than Verilog did a year after Cadence Design Systems Inc. opened that language. "We're building a foundation, not only with Synopsys but [with] many other EDA companies, for a complete verification solution," he said.

An OpenVera 2.0 tutorial is available online at www.EEdesign.com.