Synopsys' Verification Seminar Series

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.7, Item 9.0)

From: Srinivasan Venkataramanan

Last week I attended a Verification Seminar from Synopsys (They are
conducting a series of it worldwide and was held @ Leela Palace,
Bangalore on April 1st). Please find my comments/remarks about the
same herewith, please consider circulating it in your next Verif Guild
post.

Overall the seminar was quite good and also the followup of user
queries is good (I just received a call from them on one of my
queries). As with any other event I am trying to capture the negative
points in a hope that these will be avoided in future events.

There was too much hype about the OVA, I understand it is a "Synopsys"
seminar and that too free of cost, but it does eat up a whole day of
about 100+ engineers, so I hope that a company like Synopsys will
respect the value of that time. OVA is merely the temporal portion of
a HVL, and we all knew that Specman-E's temporal part was more
powerful (I remember some threads in Janick's Verif Guild on this) and
what adds to OVA is a "set of pre-built assertions" - which I agree is
good, but can be replaced with OVL, which is pure Verilog/VHDL and
hence is "native" not just to VCS but to any Verilog simulator.

When asked about more "native" support to OVL, they said "No Plans" -
I don't understand why, it will surely benefit their customers if they
support multiple standards, especially things like OVL is not all that
hard to support (I guess - I am NOT a EDA Developer).

Another thing that annoyed me was that they claimed that the upcoming
IEEE PSL (Property Specification Language) will be more of OVA and
little bit of Sugar etc. The fact is that Accellera picked up IBM's
formal property language as standard - which is Sugar and they are
adding the best of other worlds such as E, Open VERA, CBV etc. There
was an article on EETimes on this, please refer to:
http://www.haifa.il.ibm.com/projects/verification/sugar/EEDesign-Accellera.htm
On the contrary, the presenter said "Sugar is NOT accepted by
Accellera" even after the audience raised doubts on that claim. Though
I agree that Synopsys will try and promote OVA, giving false
information such as this to a large audience should be avoided,
IMHO. And just to add more support to Sugar as a base, here is what I
read from http://www.eda.org/vfv/overview.htm

---------------------------------------
1.3 FPL Selection
In April 2002, the FPL Committee selected Sugar 2.0 from IBM as its
base for standardization.
---------------------------------------

Another +ve argument to support OVA was that it is available "today"
and hence the users don't need to wait..but I know that Cadence's LDV
4.1 has limited support to Sugar based assertions and a REAL GOOD
Simvision debugging environment to Debug any failing assertions.

- Srinivasan Venkataramanan, Intel

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.7, Item 9.1)

From: Bernard Deadman

Neal's question opens up a lot of issues associated with
Assertion-based Verification, not the least being the issue of IP
protection, which is typically more difficult in the PSL/Sugar & OVA
based solutions, and doesn't seem to have been considered for
SystemVerilog Assertions. The problem is it takes a considerable
amount of effort to comprehend the protocol and to generate this
material, therefore I doubt few users will be willing to give away,
for example, a carefully honed set of assertions for PCI-X, AHB or
similar.

And even if this material were available, under the present business
models, it would be just one interpretation of the salient features of
the protocol, just as today you could buy a PCI monitor from 0-in or
one of the eVC vendors.

One of the issues that has to be faced is just how complete a job are
the set of assertions doing? So far as I'm aware nobody has yet
figured out a way to measure the completeness of either packaged
monitors or sets of assertions.

If you look at typical protocols, these are described today using
ambiguous 'English', illustrated with a selection of representative
waveforms. I'm sure readers can recount cases where groups have
created different functionality by reading different semantics into
ambiguous descriptions. This is different from the standardization
process for, say, the Verilog, VHDL, PSL/Sugar etc. languages, all of
which, in the 21st Century, are standardized using the Backus-Naur
Format (BNF) that explicitly defines the allowable sequences of tokens
within a language.

It seems to me the solution is for all of us to insist we can no
longer afford the luxury of "English" protocol descriptions, with
reliance on IP houses like Synopsys, Denali, 0-In, etc. to
re-interpret the spec. by building monitors. Instead we should be
looking to the bodies that standardize everything from PCI to SCSI to
Infiniband as well as semi-proprietary protocols such as AMBA and
CoreConnect as well as internal describing unpublished block-to-block
communications, to transition to unambiguous formal temporal
definitions.

I advocated this in a DVCon tutorial (you can find the slides at
www.sdvinc.com/PSL-Sugar_tutorial_pt5.pdf ) where you'll see I've
demonstrated how this can be done using Regular Expressions based on
PSL/Sugar, including the ability to scale the concept to protocols
such as Infiniband, and I'll gladly talk through the details with
anyone who's interested.

As the transition to formal protocol description takes place, tools
use this material as source to automatically generate the monitors,
checkers, BFM's, transactors, TVM's, assertions etc. that Neal and the
industry needs, in days rather than months, and with substantially
better accuracy than the present hand-coded interpretations.

I really believe the formal description of protocols is the easier way
forwards that Neal is looking for, because the standards bodies
improve the quality of their output and the users enjoy a paradigm
shift from business models that stress payment per simulation to
solutions where the material is readily available on a per-protocol
basis.

Well, I always did have an idealistic streak....

- Bernard Deadman, SDV Inc

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.8, Item 13.0)

From: Anonymous

As it happens, your Synopsys rep was probably right. To understand
why, you'll need to know what's been going on in Accellera for the
past few years. First, a disclaimer: I have no current, or past,
connection with either Accellera or any of the companies who were
involved in the PSL standardisation process. I believe the information
here to be correct; it is all in the public domain, and can be easily
checked.

OVI started work on a formal property specification language over 4
years ago. OVI and VHDL International later merged into Accellera,
and the Accellera Formal Verification Technical Committee (FVTC)
started work in earnest in October 2000. The FVTC sought language
donations as a basis for their work, and Verisity, Motorola, and IBM
donated temporal e, CBV, and Sugar, respectively. Some months later -
technically after the expiry of the submissions deadline - Intel
donated ForSpec. Synopsys was involved in the FVTC at this stage, but
chose not to make a language donation. The FVTC spent the next year
evaluating the 4 donations and, in December 2001, carried out a
balloting process that eliminated the 'e' and ForSpec donations,
leaving only Sugar and CBV as candidates for the Accellera PSL. At
this point, the FVTC defined a number of features they would like to
see in the PSL, and IBM and Motorola modified their submissions to
bring them closer to the FVTC requirements. Eventually, in April 2002,
a final ballot was carried out, and Sugar 2.0 was selected, by a large
margin, as the Accellera Formal Property language. The name 'PSL' was
coined at a later date. This should have been pretty much the end of
the matter, and the FVTC at this time was only concerned with creating
an LRM for Sugar 2.0, and subsequently submitting it to the IEEE for
standardisation.

However, this is where things start to get interesting. Back in
November 2001 Intel had made a press release which, with the benefit
of hindsight, should have told the FVTC that they were in trouble. The
story is still at . The
story basically said that Intel had recruited Synopsys, Verisity, and
Co-Design to back ForSpec. Synopsys agreed to add ForSpec to OpenVera;
Verisity agreed to add parts of ForSpec to 'e'; and Co-Design agreed
to add ForSpec to Superlog. This didn't impress the FVTC, and the
members voted a month later to eliminate first 'e', and later ForSpec,
from consideration, for technical reasons. Interestingly, Verisity
itself voted against 'e' when it was given a choice between 'e' and
ForSpec in the December ballot.

That's the first half of the interesting bits. The second half is that
Accellera is also responsible for SystemVerilog. SystemVerilog, you
will remember, is based on Co-Design's Superlog; and Synopsys is, of
course, the prime mover behind SystemVerilog. In June 2002 Synopsys
donated OpenVera Assertions (OVA) as the basis for SystemVerilog 3.1
assertions. In August 2002, Synopsys bought Co-Design. In October
2002, the SV-AC (SystemVerilog Assertion Committee) voted 6-4 to
accept the OVA donation. For the record, 4 of the 6 acceptance votes
were from Synopsys, Intel, Sun, and Motorola. These four companies
were, coincidentally, the four companies who voted against Sugar, and
for CBV, in the final FVTC ballot.

So what has all this got to do with PSL, Sugar 2.0, and the FVTC? As
it turns out, everything. Shortly after the FVTC's selection of Sugar
2.0 in April 2002, it was instructed by the Accellera board to 'unify
OVA and PSL' into a 'unified simulation kernel'. No OVA donation was
made to the FVTC; no evaluation was carried out; no vote was taken on
whether OVA might be suitable for the PSL; no account was taken of the
fact that the FVTC had already completed its deliberations, after a
period of 4 years of intense technical activity. No account was taken
of the fact that OVA did not have any formal semantics, and no
instructions were given on how it might be possible to unify these two
different languages. No account was taken of the handful of companies
which had already developed Sugar 2.0 products in anticipation of the
FVTC's deliberations. No account was taken of the fact that Synopsys
had itself participated in the FVTC process. Orders were given that
the name 'Sugar' should be dropped. In short, the Accellera board
simply ignored the (excellent) work of the technical committee, and
took control of the PSL by dictat. The original Sugar-based PSL 1.0
LRM has still not been approved by Accellera, and the FVTC continues
to integrate OVA and PSL 1.0 into what may, or may not, turn into PSL
1.1.

It seems clear that the reasons for this can only have been
political. As the Accellera Technical Committee chairman, Vassilios
Gerousis, has pointed out, "Accellera is a business oriented
standardization group." They rely on the fees of their members, and
only their 21 Corporate and Associate members are guaranteed to have
votes on technical issues.

Should any of this come as a surprise to us? Probably not. Accellera
is not an independent standards organisation, in the way that the IEEE
is. If it did not provide important funding to the IEEE it would be,
in short, an irrelevance. If there's a lesson to be learnt here, it's
that, if we expect to get good standards, then we're going to have to
pay for them ourselves.

Finally, those of us with longer memories will recall that, when
Accellera was launched, it was going "to end the language wars". Am I
the only one who can detect a hint of irony in this?

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.8, Item 13.1)

From: Bernard Deadman

I received a copy of a comment about the history of the selection of
PSL / Sugar from [Anonymous]. As a member of the FVTC committee
during this period his narrative fits very closely with the events I
remember, though I would comment:

He wrote "{after eliminating two languages} the FVTC defined a number
of features they would like to see in the PSL", whereas the way I
remember it is one of the biggest, most impressive tasks the FVTC took
on was the creation of the initial requirements spec. (a feature
suspiciously lacking in the SystemVerilog effort) together with the
coding and assessment of 70 or 80 properties written (where possible)
in all four donated languages. For me at least, that was one of the
most telling indications of which languages were good, and which were
easy to use.

During the presentations prior to the selection process all the
donating teams proposed changes to their languages to increase
conformance with the requirements spec. There were subsequent rounds
of refinement when the selection was between Sugar & CBV and again
after the selection of Sugar and while the final LRM was being
produced.

Overall this was one of the best thought out pieces of language
selection, refinement and definition I've seen and substantially in
advance of the vendor dominated SystemVerilog approach of tossing out
technical features to hit arbitrary commercial deadlines.

In addition a number of statements were made at the stormy Accellera
open meeting at DAC 2002 (
http://www.eedesign.com/story/OEG20020611S0035 - notice the quote from
Francine Ferguson) about consideration of the acceptance of the OVA
which were simply not adhered to. Despite statements to the contrary,
acceptance of OVA as a key component of SystemVerilog was a decision
made without reference to the FVTC, even though Sugar 2.0 has more
capability, formally defined semantics and has been proven to span
both assertions in simulation *AND* Formal Verification (static Model
Checking).

In the end PSL/Sugar was in danger of being "dumbed-down" to the
lowest common denominator to fit political ends, which is why I no
longer have the patience to listen to proclamations from on high by
the Accellera TCC. IMHO that's *NOT* the way to design 21st Century
languages!

- Bernard Deadman, SDV Inc.

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.8, Item 13.2)

From: Bala Sreekandath

As one of the organizers of the Synopsys Verification Seminar in
Bangalore, I would like to both thank Intel's Srinivasan for his
attendance and overall feedback that the seminar was good. I also
appreciate his candor and can understand the confusion regarding
assertions and the language standard status.

OpenVera Assertions (OVA) is an open high-level verification language
that enables an assertion-based methodology. It was created by Intel
and Synopsys and has been donated for consideration for SystemVerilog
assertions. The OVA language contains easy-to-use, powerful
declarative constructs which you can use to create complex protocol
and other checkers. It's useful for simulation and can drive a
variety of verification tools including property checking and
hardware-assisted verification - but rather than compare the power and
usefulness of different assertion languages, I will point out AMD's
comments made at the seminar stating that using OVA native in VCS they
"found bugs that would have otherwise gone undetected".

As pointed out in the post, VCS and other Synopsys verification
products do ship with a "set of pre-built checks" (called the "OVA
Checker Library"), which is good for quickly ramping up. However,
more interesting for most verification engineers is the selection of
IP (see http://www.open-vera.com) and also the flexibility to write
"custom" assertions to concisely capture the intent of very complex
functionality.

In regard to the OVL, since it is written in Verilog it is already
"native" to VCS. Any "plans" for enhancement would come from
Accellera, not Synopsys. In contrast to OVL, using checks from the
OVA Checker Library benefits users with better debug and integration
with assertion coverage with tools that provide OVA support such as
VCS, VCS MX, Vera, and others.

The comments from our presenter regarding Accellera's PSL (not IEEE as
stated in the post) may have been misunderstood. His response to an
attendee's question was "Sugar is not a standard by Accellera".
Synopsys understands the current status (at the time of this post) of
SystemVerilog 3.1 with assertions and PSL 1.0 is that they have been
passed by the technical committees and have been submitted for
approval by the Accellera board. Accellera made the PSL plan clear at
its public seminar held on December 4, 2002 in Santa Clara, California
- based on membership feedback, SystemVerilog 3.1 assertions and PSL
1.1 will share a common, 'unified set' of assertions constructs. This
unified approach tremendously benefits the engineering community since
almost no one wants to use one language for simulation and another for
formal.

I know there is a lot of discussion regarding the status of the
standards, and therefore invite all readers to become involved with
Accellera's standards effort and to check with their company reps on
the various technical committee activities. Once SystemVerilog 3.1 is
standardized (targeted for June 2003) and PSL with its unification
with SystemVerilog assertions becomes a standard, we look forward to
moving onto more interesting discussions regarding new verification
methodologies and tools.

- Bala Sreekandath, Applications Consulting Manager, Synopsys