Questa AVM

[HT-Lab]

Sorry, but this claim doesn't hold any water. Saying most features are
not used a lot (provided that your assumption is true to begin with),
cannot imply that other features might not be used either.

What I meant with this remark is that there is a lot of capability left in
VHDL for verification engineers yet some presenters (I mistakenly
generalised this to EDA companies) wants to make us believe that we should
throw away VHDL and start from scratch with SystemVerilog. This is IMHO not
true and you can create a powerful verification environment using VHDL and
OVL (or PSL if you can affort it).

Really? Of the four quoted features only one is available in VHDL (and
ironically neither in SV core or std package), none in Verilog. How's
that "most of these"?

Assertions : PSL (with nice VHDL or Verilog language flavours) or you can
use the free OVL.
Fixed Point : (and floating point) are available for VHDL in a separate
packages (included as standard with Modelsim).
CR : You can do Constraint Random in VHDL but there is no solver so yes this
takes extra programming effort. If you want to use a free constraint solver
and are willing to learn bit of SystemC than you can use OSCI to stream CR
data via pipes/sockets to your simulator.
TLM: see paper by Jim Lewis :
http://synthworks.com/papers/VHDL_Subblock_Verification_DesignCon_2003_P.pdf
OO: Not available.

Hans
www.ht-lab.com

Regards
Marcus

--
note that "property" can also be used as syntaxtic sugar to reference
a property, breaking the clean design of verilog; [...]

(seen on http://www.veripool.com/verilog-mode_news.html)

 

[KJ]

I'm kinda missing how an assertion statement is not *standard* and how it
would be any easier to parse some improved 'standard'. VHDL has had
assertions since 1987....and welcomes other languages to the assertions
club.

[...]

We must have completely different ideas of assetions then. An assertion
(in
any form) is a statement of something that must by golly be true....if it
is
ever not true an error has occurred. Plain old assertions are used to
specify protocols and interface behavior as well as very
design-specific-probably-of-no-use-to-anyone-else-but-this-design types
of
things.

I guess so. When people talk about "assertion based verification" they
don't usually mean the VHDL "assert" statement.

I wasn't discussing 'assertion based verification' and never said that it in
any way equates to a VHDL assert statement though. What I was responding to
was Petter's statement....

My point is having a *standard* way of specifying assertions (like SVA).
Then formal tools could read and easily (or at least easeier than
analyze assertions written in any HDL form) analyze the assertions in...

and I simply questioned how he thought that VHDL asserts are not
standardized or how they could not be used to do the same thing that he
implied could best be done with SVA.

A VHDL assert is the basis on which all VHDL tool based verification occurs
within the VHDL language. One can use that basis along with the other
language constructs to build up either generally applicable canned
verification procedures (for example PSL) or sprinkle your asserts
throughout the design and testbench as appropriate for a design specific set
of assertions to verify your design.

You are right in that
an assertion states what is the supposed behavior. However, the
expression that is evaluated differs significantly from what is tested
in a VHDL "assert" statement.

In every language that I've run across the asserted expression must evaluate
to some form of boolean expression which is either 'true' (good) or 'false'
(bad, exception, etc.).

Assertion languages like PSL, SVA or /e/
verify temporal behavior.

Only if you take the view that a VHDL assert must be a simple concurrent
statement. A whole slew of VHDL asserts can be placed anywhere in
procedural code as well and verify that an entire sequence of events is
happening properly (which is what I think you mean by 'verify temporal
behavior').

PSL, as an example, needed no VHDL language extensions to support it. PSL
simply packages up some generally applicable things to verify and asserts
that they happen properly. You instantiate them apprropriately to verify
whatever it is your design is doing. Personally I don't find them that
useful to use since I find it easier to embed the thing that I'm asserting
in the design and/or testbench. I've also written standalone interface
protocol verifiers when appropriate.

KJ

 

[KJ]

Got my standards confused....meant to say OVL in the earlier post, not PSL
as far as not needing any language extensions.

 

[HT-Lab]

Care to give an example to demonstrate how it is any more powerful than a
VHDL or PSL assertion? I'm guessing that it will turn out to be just

I did not claim that it was more powerful, but it's easier for tools
to interpret since it's located in an assert statement like:

assert property (@(posedge Clock) Req |-> ##[1:2] Ack);

Just to make sure VHDL users don't stray into the dark SVA side here is
the VHDL flavoured PSL version (assuming ##[1:2] means 1 to 2 clockcycles?):

property xxx is always ({Req} |-> {[*1:2];Ack}) @ rising_edge(Clock);
assert xxx;

Hans
www.ht-lab.com

--
A: Because it messes up the order in which people normally read text.
Q: Why is top-posting such a bad thing?
A: Top-posting.
Q: What is the most annoying thing on usenet and in e-mail?

MI5 postings!

 

[Petter Gustad]

Care to give an example to demonstrate how it is any more powerful than a
VHDL or PSL assertion? I'm guessing that it will turn out to be just

I did not claim that it was more powerful, but it's easier for tools
to interpret since it's located in an assert statement like:

assert property (@(posedge Clock) Req |-> ##[1:2] Ack);

In plain VHDL or Verilog you can write your assertions in so many ways
that it's difficult for other tools to extract and interpret them.

Petter

 

[Mike Treseler]

Just to make sure VHDL users don't stray into the dark SVA side here is
the VHDL flavoured PSL version (assuming ##[1:2] means 1 to 2 clockcycles?):

property xxx is always ({Req} |-> {[*1:2];Ack}) @ rising_edge(Clock);
assert xxx;

OK, I'll bite.

I could add a short procedure to my vhdl
testbench library to check the same thing,
*and* I could debug that code by stepping and watching.

Why do I need yet another language, and if
I did, how would I debug such an assertion
when it doesn't fire as I expect.

-- Mike

 

[Marcus Harnisch]

Hi Hans

...yet some presenters (I mistakenly generalised this to EDA
companies) wants to make us believe that we should throw away VHDL
and start from scratch with SystemVerilog.

Staying with VHDL as a design language is not a bad thing at
all. Combining it with SV for verification is not a bad thing
either. Only time will tell if and when SV takes over.

...you can create a powerful verification environment using VHDL and
OVL (or PSL if you can affort it).

OVL is just for basic things and not exactly readable. You could argue
that regular expressions are not readable either and we'll kick off an
endless thread. PSL -- while powerful -- was designed to be language
agnostic but even the "VHDL flavor" didn't really look like VHDL. Also
it doesn't seem to be integrated too well into (current) VHDL.

Assertions : PSL (with nice VHDL or Verilog language flavours) or you can
use the free OVL.

See above.

Fixed Point : (and floating point) are available for VHDL in a separate
packages (included as standard with Modelsim).

What I meant was *SV* doesn't have fixed point. I know that it is
available for VHDL of course.

CR : You can do Constraint Random in VHDL but there is no solver so yes this
takes extra programming effort.

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

If you want to use a free constraint solver and are willing to learn
bit of SystemC than you can use OSCI to stream CR data via
pipes/sockets to your simulator.

SCV is not nearly as powerful as any core language CR mechanism as
provided by SV and /e/. Worse: It's C++ syntax. I wonder when the
first SystemBrainfuck implementation hits the market. Goodness
gracious, don't you think that Verilog is bad enough?

Regards
Marcus

 

[Marcus Harnisch]

I could add a short procedure to my vhdl
testbench library to check the same thing,
*and* I could debug that code by stepping and watching.

Of course you could use your own testbench library. But does it make
sense? You would end up writing rather complex finite automata to
implement the whole bloody thing.

When someone suggests using grep(1) to match some reasonably complex
text pattern would you respond that regular expressions are not really
needed, since you could reimplement the pattern matching code in C
rather quickly?

As far as debugging is concerned, tools have generally good support
for assertions, showing you the current state of assertions
(active/failure/success). Needles to say that this applies to multiple
assertion threads as well. I doubt debugging is that well supported
with any testbench library in either Verilog or VHDL.

Regards
Marcus

 

[Mike Treseler]

Of course you could use your own testbench library. But does it make
sense? You would end up writing rather complex finite automata to
implement the whole bloody thing.

Checking for ack after one or two ticks
does not seem that complex to me.

When someone suggests using grep(1) to match some reasonably complex
text pattern would you respond that regular expressions are not really
needed, since you could reimplement the pattern matching code in C
rather quickly?

When there is at tool that allows me
to grep my code for functional errors,
I will buy it.

As far as debugging is concerned, tools have generally good support
for assertions, showing you the current state of assertions
(active/failure/success). Needles to say that this applies to multiple
assertion threads as well. I doubt debugging is that well supported
with any testbench library in either Verilog or VHDL.

Setting vsim breakpoints and watching locals and objects
works well for debugging. I use assertions after
the code is working. I will agree that we disagree.

-- Mike Treseler

 

[HT-Lab]

Just to make sure VHDL users don't stray into the dark SVA side here
is
the VHDL flavoured PSL version (assuming ##[1:2] means 1 to 2
clockcycles?):

property xxx is always ({Req} |-> {[*1:2];Ack}) @ rising_edge(Clock);
assert xxx;

OK, I'll bite.

I could add a short procedure to my vhdl
testbench library to check the same thing,
*and* I could debug that code by stepping and watching.

Why do I need yet another language, and if
I did, how would I debug such an assertion
when it doesn't fire as I expect.

-- Mike

Hi Mike,

You are right that you can implement this in VHDL, however, the point is
that with a formal tool you can find out if this property hold exhaustively
under any circumstances (something which could be impossible with a
testbench). To give you some more examples, it only takes one simple
property to exhaustively prove that a statemachine is always onehot or that
it always recovers from an illegal state.

With assertion languages you can also write properties like "if A has
happened than B must have happen sometime in the past", this is very
difficult to capture in any HDL language. I can go on and on, the point is
that assertions languages are extremely powerful and this is not just
because of the concise language syntax but obviously also because of the
available formal tools. If there was no capacity issue with formal tools we
all be writing assertions instead of testbenches

The only thing we need now is affordable assertions and VHDL2006!

Regards,
Hans
www.ht-lab.com

 

[Petter Gustad]

I wasn't discussing 'assertion based verification' and never said that it in
any way equates to a VHDL assert statement though. What I was responding to
was Petter's statement....

My point is having a *standard* way of specifying assertions (like SVA).
Then formal tools could read and easily (or at least easeier than
analyze assertions written in any HDL form) analyze the assertions in...

You cut off a significant part of my sentence here:

"My point is having a *standard* way of specifying assertions (like SVA).
Then formal tools could read and easily (or at least easeier than
analyze assertions written in any HDL form) analyze the assertions in
conjunction with the coverage results and possibly generate vectors to
improve the coverage."

The combination of assert and covergroups is essential.

Petter

 

[HT-Lab]

Hi Hans

"HT-Lab" <[email protected]> writes:

... snip..

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

I am not talking about implementing a solver in VHDL but to manually filter
the random data. This is something you can do in VHDL.

SCV is not nearly as powerful as any core language CR mechanism as
provided by SV and /e/.

That is unfortunately true.

Worse: It's C++ syntax.

C++ is not that bad, I must agree that I still do all my general programming
in C but by using SystemC I have come to appreciate the finer points of C++.
As one would say, "once you are over the hill you will begin to pick up
speed".

wonder when the
first SystemBrainfuck implementation hits the market.

And then we have to start a whole new thread again when some presenter
remarks that we have to look for some other profession if we are not
thinking of updating ourselves with SystemBrainfuck .

Regards,
Hans
www.ht-lab.com

Goodness
gracious, don't you think that Verilog is bad enough?
Regards
Marcus

--
note that "property" can also be used as syntaxtic sugar to reference
a property, breaking the clean design of verilog; [...]

(seen on http://www.veripool.com/verilog-mode_news.html)

 

[JK]

And then we have to start a whole new thread again when some presenter
remarks that we have to look for some other profession if we are not
thinking of updating ourselves with SystemBrainfuck .

Regards,
Hanswww.ht-lab.com

Regards,
JK

 

[Andy]

HT-Lab wrote:

Just to make sure VHDL users don't stray into the dark SVA side here
is
the VHDL flavoured PSL version (assuming ##[1:2] means 1 to 2
clockcycles?):
property xxx is always ({Req} |-> {[*1:2];Ack}) @ rising_edge(Clock);
assert xxx;

OK, I'll bite.

I could add a short procedure to my vhdl
testbench library to check the same thing,
*and* I could debug that code by stepping and watching.

Why do I need yet another language, and if
I did, how would I debug such an assertion
when it doesn't fire as I expect.

-- Mike

Hi Mike,

You are right that you can implement this in VHDL, however, the point is
that with a formal tool you can find out if this property hold exhaustively
under any circumstances (something which could be impossible with a
testbench). To give you some more examples, it only takes one simple
property to exhaustively prove that a statemachine is always onehot or that
it always recovers from an illegal state.

With assertion languages you can also write properties like "if A has
happened than B must have happen sometime in the past", this is very
difficult to capture in any HDL language. I can go on and on, the point is
that assertions languages are extremely powerful and this is not just
because of the concise language syntax but obviously also because of the
available formal tools. If there was no capacity issue with formal tools we
all be writing assertions instead of testbenches

The only thing we need now is affordable assertions and VHDL2006!

Regards,
Hanswww.ht-lab.com

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?

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. For instance if you're
not supposed to be in state x unless something else has happened, then
put an assertion statement in the code for state x that verifies
something else has happened.

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. I suppose the bolting-on approach has
merit when you are not verifying your own code, but otherwise, it is
yet another syntax that has to be understood.

Maybe we need a new paradigm for verification (and even applicable to
SW test), whereby the source level debugger allows you to insert
assertion and other benign statements the same way you can insert
breakpoints...

Andy

 

[Mike Treseler]

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?

Yes. If solver vendors wish to sell to vhdl users, throw us a bone.

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. For instance if you're
not supposed to be in state x unless something else has happened, then
put an assertion statement in the code for state x that verifies
something else has happened.

A low budget way to do something like this in vhdl
is to declare a variable (or signal if you must)
that is is never assigned to an output port,
but calculates an interesting (but non-synthesizable)
reference value to verify some complex, pipelined synthesis
procedure. Simulation just runs it. Synthesis either
ignores it or throws a warning.

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. I suppose the bolting-on approach has
merit when you are not verifying your own code, but otherwise, it is
yet another syntax that has to be understood.

In some organizations, the designer and the verifier
are the some person.

Maybe we need a new paradigm for verification (and even applicable to
SW test), whereby the source level debugger allows you to insert
assertion and other benign statements the same way you can insert
breakpoints...

I'll take one of those, please

-- Mike Treseler

 

[KJ]

Andy wrote:

A low budget way to do something like this in vhdl
is to declare a variable (or signal if you must)
that is is never assigned to an output port,
but calculates an interesting (but non-synthesizable)
reference value to verify some complex, pipelined synthesis
procedure. Simulation just runs it. Synthesis either
ignores it or throws a warning.

Not sure I follow your suggestion, unless it is to compute some form of
checksum/CRC/etc. on some (all) of the inputs and outputs and then compare
it (presumably with an assert) to some golden reference value. If that is
the gist of it, then it would seem to not be of much value while you're
still developing the code (since the golden reference will change with every
functional change....presumably). After development is 'done', I'd much
rather be still using version control to check for what changed, rather than
trying to figure out whether the reason for a bad checksum/CRC/etc. is due
to a design change in that module or simply a change in the usage of that
widget (i.e. the inputs are acting differently now).

Plus it might be a bit difficult to develop such an interesting reference
value for an entity that is used in more than one place since the golden
reference value could be different for each usage....or am I just missing
something here?

Kevin Jennings

 

[Thomas Stanka]

You can write assertions in any language, even plain old Verilog. My
point is having a *standard* way of specifying assertions (like SVA).
Then formal tools could read and easily (or at least easeier than
analyze assertions written in any HDL form) analyze the assertions in
conjunction with the coverage results and possibly generate vectors to
improve the coverage. Assertions used like this is more a
specification of protocols and interfaces rather than an error message
to tell you that something went wrong.

I think I understand your point. You would like to have a unique way
for an assertion that is understood by all tools. I wonder if this
will be ever true, as I see no tool at the moment supporting full SV
and no tool doing this task for VHDL.
In fact I have no idea if SV helps the tool designer in reaching this
task, or if it is only the commercial point of selling new tools to
companies allready having a complete toolset, that drives the EDA
companies to enforce SV against VHDL.

bye Thomas

 

[Kim Enkovaara]

I think I understand your point. You would like to have a unique way
for an assertion that is understood by all tools. I wonder if this
will be ever true, as I see no tool at the moment supporting full SV
and no tool doing this task for VHDL.

SVA part is well supported in the tools, and even the different
graphical debug features are quite advanced.

And at least in Questa you can bind SVA assertions to VHDL code.
I would be suprised if other major simulators would not support
that.

In fact I have no idea if SV helps the tool designer in reaching this
task, or if it is only the commercial point of selling new tools to
companies allready having a complete toolset, that drives the EDA
companies to enforce SV against VHDL.

Usually if you have the complete toolset these features are embedded
there without any major extra cost or for free. They are just part
of the mixed language and system verilog implementations.

Formal tools are then another layer, but also there standard
languages are just replacing the proprietary languages. Then there
are some interesting tools coming that synthesize assertions and
you can get assertion, coverage etc. information from the final
chips. That can be a huge time saver in debugging the designs.

--Kim

 

[Mike Treseler]

Not sure I follow your suggestion, unless it is to compute some form of
checksum/CRC/etc. on some (all) of the inputs and outputs and then compare
it (presumably with an assert) to some golden reference value.

Nothing fancy as that. Just a sim reference value in the RTL.
Some function of local variables that the testbench can't see.

-- Mike Treseler

 

[HT-Lab]

Thomas Stanka wrote: ...snip

Formal tools are then another layer, but also there standard
languages are just replacing the proprietary languages. Then there
are some interesting tools coming that synthesize assertions and

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...

you can get assertion, coverage etc. information from the final
chips. That can be a huge time saver in debugging the designs.

Indeed, there are some assertions that simply cannot be proven by any formal
tool due to the large cone of logic, in this case you synthesise your
assertion to a hardware monitor and embed it on your prototype.

Hans
www.ht-lab.com