Questa AVM

[Marcus Harnisch]

Hi Andy

Can't most formal tools "prove" regular VHDL-87 assertions? So we
beg, borrow or steal a package of functions/procedures that can be
called in conjunction with an assert statement to accomplish all these
new-fangled properties?

This is pretty much how OVL is implemented. Better than nothing, but
not what I would prefer over a real assertion language.

What is nice about assertion statements (and maybe properties; I don't
know) is that they can be placed inside existing conditional
statements, etc. in you regular code, so you don't have to separately
account for those conditions in the property.

Sometimes this is exactly what you want to have. Diversity gives you a
better chance of catching bugs early. Introducing the same bug in two
entirely different solutions (RTL and PSL/SVA) is rather difficult.

Compare that to comments. We all carefuly comment our code, don't we
Why? Isn't the RTL description sufficient? Anyone reading well
written code knows immediately how a device will behave. In fact some
argue that comments in code are dangerous because nothing ensures that
they are up-to-date with the code they are supposed to describe, hence
causing more confusion that they were to solve. If you look at some
mature projects you will find some truth in that.

If you consider assertion languages as "formal comment" you'll get two
benefits:

1. Assuming a sufficiently complete test environment you'll get
feedback if comment (assertion) and code diverge.

2. A well specified formal language doesn't leave room for
interpretation. Prose is ambiguous, assertions are not.

Plus, if used in specifications (instead of or alongside timing
diagrams and prose), you can now easily verify the actual behavior
vs. specifed behavior.

Maybe it's just me, but it seems like properties were developed for
"bolting on" verification, where as I think we need to do more
"building in" verification.

Deliberatly in a way. To provide diversity (see above), and to get a
concise way to describe some behavior.

Regards
Marcus

 

[HT-Lab]

..

These tools have been available for a while (more than a year at least). I
believe Temento's Dialite was one of the first that synthesized PSL to
hardware (now also supports SVA).

http://www.temento.com/index.php

Their website seems to be down at the moment...

Website is back up again, for those of you who are interested have a look at
this paper :

http://www.temento.com/data/whitepaper/AssertionsForDesignandVerification2.pdf

Hans
www.ht-lab.com

 

[Paul Taylor]

Compare that to comments. We all carefuly comment our code, don't we
Why? Isn't the RTL description sufficient?

Coding of something is a divide and conquer task, and apparently the magic
number in terms of splitting a problem up is seven. Commenting lumps of
code helps to compartmentize it, and therefore helps understanding.

Anyone reading well
written code knows immediately how a device will behave.
In fact some
argue that comments in code are dangerous because nothing ensures that
they are up-to-date with the code they are supposed to describe, hence
causing more confusion that they were to solve.

I've done that

If you look at some
mature projects you will find some truth in that.

If you consider assertion languages as "formal comment" you'll get two
benefits:

1. Assuming a sufficiently complete test environment you'll get
feedback if comment (assertion) and code diverge.

In which case, can't we just compile the comments ;-)

Regards,

Paul.

 

[Mike Treseler]

In which case, can't we just compile the comments ;-)

Or maybe compile those high-level powerpoint bullet items directly.

-- Mike Treseler

 

[Jim Lewis]

Marcus,

You just cannot have constrained random without a solver. And "extra
programming effort" doesn't get you one.

I would disagree.

What declarative based constrained random (like SV class based)
attempts to do is solve all constraints simultaneously so that
you get uniformity across an entire solution set.

So for a simplistic problem (borrowing from Chris Spear's SV book)
and making the specification language independent:
randomize X in (0, 1)
randomize Y in (0, 1, 2, 3)
constrain Y such that if X is 0, then Y must be 0

The theory is that the solver will give you a uniform set
solution values to the above:

X Y probability
0 0 20% = 1/5
0 1 0
0 2 0
0 3 0
1 0 20 %
1 1 20 %
1 2 20 %
1 3 20 %


What VHDL supports is procedural randomization. With procedural
randomization you construct your constraints in your code.
For example:

RandomGenProc : process
variable RandomVal : real ;
variable S, X, Y : integer ;
variable seed1 : positive := 7 ;
variable seed2 : positive := 1 ;

begin
. . .
for i in 1 to 1000 loop
-- Randomize: RandomVal is in the interval of 0.0 to 1.0
uniform(seed1, seed2, RandomVal) ;

-- Scale: Range 0 to 4
S := integer(trunc(RandomVal*5.0)) ;

-- Case distribute (gen X = 0 20% , and X = 1 80 %)
case S is
when 0 =>
X := 0 ;
Y := 0 ;

when 1 to 4 =>
X := 1 ;
-- Gen Y in 0 to 3
uniform(seed1, seed2, RandomVal) ;
Y := integer(trunc(RandomVal*4.0)) ;

when others => report "Can't get here" severity failure ;
end case ;

ApplyStim(Rec, X, Y) ;

end loop ;
end process ;

This demonstrates that with a little of work and apriori
thinking about the set of values, then we can _often_ do
constrained random procedurally. While you may be able
to find some examples where procedural approach will not
work, I have found that I generate all of the test cases
I need. I would be interested to see any examples
that you either use or would like to use for verification
and you don't think it can be done using the procedural
based approach.

It would be nice to be a little more concise and I have a
package that does just that. Had DVCon accepted my paper,
I would be releasing it then. Instead, I am working on a book
that documents how to do this, verification data structures
such as scoreboards (re-usable and parameterizable ones), and
improvements on the record communication. The book
will take some time since I also have a day job, so for
now if you really want to know, one can take our
VHDL Testbenches and Verification class.

Going back to the SV class based randomization, I note that
Chris's book (P151, Table 6-3) does not show uniform distribution.
When I asked Chris about this he said he was posting the results
of a fast solver (in a commercial SV simulator) that apparently
takes some liberty and he insisted it was not a typo.

The point being that perhaps declarative randomization (SV) takes
enough time that vendors are concerned about speed and some of them
provide alternate solvers (perhaps also by default) that do not
produce uniform distributions. So maybe the procedural approach
will both produce more uniform results and run faster .
Time will tell.

A note about assertions. Accellera VHDL-2006 integrated PSL into
VHDL. As an Accellera standard, vendors should be implementing to
this now. It is most likely that this will become an IEEE 1076-2008.

The Accellera extensions committee has initial proposals for OO and
randomization proposals in place. What we need to finish this work
is funding for the editing and use case generation. If your organization
can help with this, please drop me a private email ([email protected]).
Also we need you to voice your opinion to your EDA vendors.
Since VHDL already has many of the necessary constructs, the level
of effort to extend VHDL will be much less than the effort it took
to make Verilog into SystemVerilog.

Best,
Jim Lewis
Director of Training, SynthWorks
IEEE VASG Chair

 

[Marcus Harnisch]

Hi Jim

Sorry for the late reply.

[the same stuff as about a year ago]

We've been through exactly the same discussion before in this group
and concluded that we will continue to disagree on that subject. I
will not repeat all my arguments once again but one thing:

I do have great respect for what you have shown is possible within the
possibilities of current VHDL. But this is far from constrained random
verification and not nearly as powerful.

Best regards
Marcus

 

[Marcus Harnisch]

Or maybe compile those high-level powerpoint bullet items directly.

Don't laugh. AFAIK people are in fact working on something like that:
Synthesis of assertion.

Regards
Marcus

 

[KJ]

Don't laugh. AFAIK people are in fact working on something like that:
Synthesis of assertion.

Synthesizable Prolog...I think I still have my TurboProlog diskettes

http://www.google.com/search?hl=en&q=Synthesizable+Prolog


Kevin Jennings