Subject: Re: problems with current definition/document
From: Adam Krolnik (krolnik@lsil.com)
Date: Mon Jul 22 2002 - 09:08:36 PDT
Good morning all;
Cindy wrote:
>4. sv-assertions should have no side effects
>justification:
> we must ensure that the design itself complies with the assertions. if
> an assertion has side effects, then there is no way to know whether
> or not this is so.
>4. the current definition seems to allow the use of assertions in such a
>way that the design itself is affected. for instance, consider this example,
>slightly modified from
> page 46:
> always @(posedge clk)
> if (state == REQ)
> b7: assert(req1)
> @(posedge clk) assert(gnt)
> @(posedge clk) assert(!req1);
> state = #1 WAIT;
> i am not sure if this is legal (and my verilog is very rusty, so
> perhaps i have syntax
There are certain advantages to using the temporal expression within
assertions for verification codes. I have written monitors that used
the temporal expressions from assertions to detect events in the
hardware and send the proper data to the monitor. Another example is
the use of coverage assertions that want to perform certain operations
based on the event being found. Data may be collected, etc.
But for hardware, you are correct, assertions are expected to have no
side effects. A simulator may even choose to not implement assertion
simulation if desired and this thus should have no negative effect on
the proper outcome (though it may have negative effects when it comes
to improper outcomes - that of taking longer to diagnose the problems.)
===========================================================================
>5. sv-assertions should be compatible with sugar
>justification:
> in the last meeting, simon (i believe it was) asked why this should be
> so, given that sv-verilog is a modeling language and sugar is a
> verification language(actually, sugar is technically a specification
> language, but that is beside the current point). my answer
> is that while sv-verilog is indeed primarily a modeling language,
> assertions are there to deal with verification issues, therefore,
> the aspect of sv-verilog that this committee is
> dealing with is verification, and it makes sense for sv-assertions and
> sugar to be mutually compatible. to put it another way: sugar provides
> a way to make standalone assertions about a design, while this sub-committee
> is dealing with defining embedded assertions. it would be extremely
> unfortunate if accellera were to come out with incompatible standards
> for these two extremely similar and intertwining goals.
Assertions have several uses:
1. Identify design intent (for humans.)
2. Ensure design intent is not violated (simulation.)
3. Prove design intent is correct (formal verification.)
4. Optimize circuit given knowledge of input state.
5. Prove equivalence of circuits with knowledge of input state.
Today, there is nothing that works for all 5. But I as a user want the
ability to write my intent and have it propagate to other tools. I do
not want to write an assertion about my design and then have to go and
translate for each tool that requires the knowledge. That situation
exists today. I can write an assertion for my code, but I have to
translate these assertions to have them proven. I can't store these
rewritten assertions in the verilog source code (where I desire them to
be since they pertain to the design.) So I have a maintenance problem -
every time the design changes, my formal assertions do not get updated.
The assertions do since they are part of the design (and fail to
lint/compile/simulate if not updated.)
IEEE1364-2001 (Verilog 2001) introduced the concept of attributes.
These attributes now give users the ability to store specific pieces of
knowledge about the design connected to explicit components of the
design. This is an open interface - you are not constrained to a
specific set of keywords or data - open.
SystemVerilog source code should also become a container for
assertions/properties. SystemVerilog should also hold the capability
to validate a design against some of these assertions. Some it may not
be able to, but there should be a method to explicitly identify these
as not being validated by a tool.
Now if you think SystemVerilog can be a container of Sugar assertions
then then there should be no difference between Sugar assertions and
SystemVerilog assertions. The user does not want (and really can't)
learn both? SystemVerilog assertions will only provide a very limited
capability. It is the equivalent of a 1.0 design. Sugar has taken the
next (and next) steps - you do want provide the most capabilities for
the users?!
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Mon Jul 22 2002 - 09:16:58 PDT