Subject: Re: Assertion requirements
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Mon Jul 29 2002 - 03:03:33 PDT
adam,
below please find some comments regarding your proposed requirements.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
>#4 Sugar Verification directives shall be simulated using assert_strobe
>semantics - they should simulate at the end of the timestep.
i do not agree with this. if sugar code can be embedded in procedural
code, then it should have semantics which are consistent with other
embedded assertions. for instance, for the following code:
always @(posedge clk)
begin
a = 3;
b = 4;
if (p)
assert (a < b);
a = 5;
end
we want the assertion to pass at all times, because at the point of the
assertion, a will always be less than b. this is consistent with the rest
of sugar, which does not dictate how time ticks, and allows reasoning about
the sequence of events as seen by an event-based simulator as well as
cycle-based clocked reasoning.
---------------------------------------------------------------------------------------
>#6 Extend Sugar to support overlapping properties with fifo semantics
> on positive directives (not including never directives)
> (so the user does not have to model fifo semantics [incorrectly].)
>
> This means that a property like "assert always req -> {[*1:10]; ack}"
> could be used safely instead of requiring fifo modeling to ensure that
two
> req's don't use the same ack as a completion event.
giving fifo semantics to the -> operator would pull the rug out from under
the whole semantic foundation of sugar. the semantics of a sugar property
at a given cycle depend only on the current and future state, not on the
past. (if you want to access past values of a signal, you must go through
the built-in function prev(), which translates past values into current
values. that is, when you access prev(a), you are accessing the *current*
value of a temporary signal which latches signal a.) now, you are
requesting that the property "always {req} |-> {[*1:10]; ack}" (i've
corrected your syntax) be dependent on the past, because in order to know
whether or not the property holds for a given assertion of req, we have to
know the history. for instance, if req is asserted at time 7, and ack at
time 8, then in order to know whether or not the property holds at time 7
according to your semantics, we have to know how many previous assertions
of req and ack there were.
to approach it from another angle, the current semantics of {req} depend
solely on whether signal req is asserted "now", while the current semantics
of {[*1:10];ack} depend solely on the next 10 cycles. you want the "|->"
operator to somehow involve putting them together in a more complicated way
than "if the left-hand side holds, then the right-hand side must hold".
that is, you want the "|->" to "know" something about the sequences on the
left and right, whereas sugar is built in a modular fashion so that "|->"
can link any two sequences to the same effect.
furthermore, you probably want the fifo semantics to say not only whether
every req got an ack, but also whether or not there were too many acks,
right? but then what happens to a simple combinatorial asertion like:
always (data_out -> data_en)
which seems to say that if we are outputting data, then the enable signal
must be asserted? in this case, it seems that it should be legal for
signal data_en to be asserted more times than signal data_out, while in
your fifo semantics, this would not be legal.
furthermore, sugar deals with finite state. putting the onus on the
implication operator as you request would seem to require that any number
of outstanding reqs are allowed (for instance, for the property always (req
-> eventually! ack), in which there is no bound on the number of cycles
between a req and its ack).
all this is not to say that i don't understand your need for a fifo
operator. my only problem is putting the load on the existing operators,
such as "->" and "|->". your proposal has generated lots of interesting
discussions internally. we haven't worked out all the details yet, but it
seems that the best way to solve this without bringing everything crashing
down around us is to provide a built-in function. either we could have a
built in function that provides the specific fifo capability, with inputs
indicating the producer and consumer signals, as well as maximum number of
outstanding reqs, etc., or provide a slightly more flexible built-in
function that counts modulo. then, you could build a property specifying a
fifo by reasoning about the number of reqs and acks modulo some maximum.
finally, i should note that it is perfectly possible to specify a fifo
today using sugar, by combining a few lines of modeling with the temporal
assertion. my understanding of your request is that you would like a way
to specify a fifo without using modeling code at all.
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
>#8. Support procedural systemVerilog assertions as if they were
>declarative and contain an antecedent equivalent to the position where
they are
>located in the code.
i don't understand this, nor do i understand the justification, in which
you say that "the example may fail falsely". i assume that by "fail
falsely" you mean "not according to the intention of the user"? i would
argue that if the user put the assertion in a combinatorial always
block, she meant something different than if she had put the assertion
in an edge-triggered always block. i can envision a case in which
assertions might be used to identify glitches caused by the event-drive
simulation, in which case you would want the glitchy behavior that i
think you are trying to avoid with this definition.
also, regardless of what you meant, it seems that you are trying to
legislate an implementation with this requirement, whereas i believe
that the assertion language should dictate "what", but not "how".
---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
>#9. Extend sugar Verification directives to include optional clocking
>specification (to override the presumed global clocking signal.)
sugar already supports clocking a property, with syntax similar to that you
are suggesting. for instance:
assert always (req -> next[2:4] ack) @(posedge clk);
specifies that after every assertion of req, ack should be asserted within
2 to 4 clock cycles.
regards,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
Adam Krolnik <krolnik@lsil.com>@eda.org on 12/07/2002 00:42:30
Please respond to Adam Krolnik <krolnik@lsil.com>
Sent by: owner-assertion@eda.org
To:
cc: assertion@eda.org, Adam Krolnik <krolnik@lsil.com>, fhaque@cisco.com
Subject: Re: Assertion requirements
Good afternoon;
Here is an initial list of requirements I would like to see.
---------------------------------------------------------------------------
#1 Add Sugar_Declaration and Verification_Directive (Sugar 2.0
Grammar productions) as an element of module_item and interface item
(SystemVerilog 3.0 grammar productions.) All productions downward
from the Sugar 2.0 productions shall be added to support the grammar.
Justification:
Regardless of whether or not a given property is simulatable,
properties
are best kept with the design source code.
They are not forgotten.
They are more readily kept up to date with the source code.
They are not lost.
They transport very easily in the source code to other places.
All tools can see them coupled with the relevant code.
RTL may be created from a file with properties already in them.
ETC.
An interface definition is a great place to put assertions/properties
to further explain how the interface is to be used and ensure that it
is used in the desired manner.
Problems with this requirement:
Some properties can not be supported in a simulation environment.
There may be some minor syntax differences between Sugar and Verilog,
that would be trivial to ammend.
The entire Sugar grammar is not necessary at the RTL level, now. But
more accomplished people will use the entire grammar.
---------------------------------------------------------------------------
#2 Provide a method to disable Sugar verification directives
(properties)
separate from the property declarations/directives. Properties not
disabled
shall be considered supported. Properties not supported shall produce
a compilation (or at the beginning of simulation - but not dynamic)
error indicating nonsupport. Properties disabled shall be ignored
(but compiled) by the tool. Properties relying on unsupported
properties
shall also produce an error indicating nonsupport.
The method of disabling Sugar verification directives shall allow for
multiple tools.
Justification:
A. Some properties can not be support in a simulation environment.
B. Commenting properties out does not provide support for other tools
that do support such properties. Different tools may support
different
sets of properties.
C. A given tool's implementation of a property may contain errors.
Different
tools will support a given property.
D. A property may be written twice in two forms (due to C.) Different
tools
would want to use one, not both.
Problems with requirement:
This could be difficult!
Maybe there should be support to override a verification directive
(e.g.
switch assert to assume) and there should be a new verification
directive to disable a property.
How do you provide support for a particular tool? Attributes ... ?
---------------------------------------------------------------------------
#3 Extend Sugar Verification directives to support the systemVerilog
merged grammar:
<Verification Directive > <pass statement> else <fail statement> ;
This allows Sugar 2.0 Verification directives to include pass/fail
statements for simulation operations.
Justification:
Assertions shall be capable of reporting a customized message with a
controllable severity.
Problems with this requirement:
Non simulation tools would have to ignore these verilog statement.
---------------------------------------------------------------------------
#4 Sugar Verification directives shall be simulated using assert_strobe
semantics - they should simulate at the end of the timestep.
Justification:
Combinatorial logic values are not stable until the end of a timestep.
Therefore a property that uses combinatorial logic (or nonblocking
assigned
register) will not operate with the correct signal values. This does
not
remove the possibility of failing a property with an incorrect signal
value.
Signals may arrive in a later timestep due to the use of modeled
delays in the
simulator. Properties in this environment would need to be run
(clocked)
with a delayed clock.
Problems with this requirement:
The systemVerilog assert statement does not use strobe semantics -
there could be
confusion if both exist. Propose an addition to add modeling delay to
clock specification?
--------------------------------------------------------------------------
#5 Extend Sugar 2.0 prev() function to support bit vectors.
Justification:
{prev(a[2], 2), prev(a[1], 2), prev(a[0], 2)} === prev(a[2:0], 2)
There is no reason to require a user to expand bit vectors to access
previous
values of a signal. This would be an impedement to usage.
Problems with this requirement:
Is there a reason Sugar does not support this?
--------------------------------------------------------------------------
#6 Extend Sugar to support overlapping properties with fifo semantics
on positive directives (not including never directives)
(so the user does not have to model fifo semantics [incorrectly].)
This means that a property like "assert always req -> {[*1:10]; ack}"
could
be used safely instead of requiring fifo modeling to ensure that two
req's
don't use the same ack as a completion event.
Justification:
In many of the examples from the FVTC there was little mention of
overlap
in the antecedents. In the Sugar 2.0 tutorial there is no
consideration of
overlapping antecedents (with the consequent sequences.) This is a
trap
waiting to spring on users. The above property can work for several
waveforms
and appear to be fine. But when events begin to occur with
variablility, it
will produce false positives.
Problems with this requirement:
This is an enhancement to Sugar 2.0, not systemVerilog.
--------------------------------------------------------------------------
#7. Replace systemVerilog temporal expressions in assertions with Sugar
Temporal_Expression (grammar production.)
This will provide compatibility between Sugar properties that exist a
declarative
elements, and systemVerilog assertions that can be procedural.
Justification:
Why support two temporal expression definitions. One is far richer and
more well
defined.
Problems with this requirement:
This is not compatible with SystemVerilog 3.0. This though is a spec
that has
only been out for a month (and will only be out for 6-8 months before
superseeded.
Sugar temporal expressions also include components not supportable in
a simulation
environment.
--------------------------------------------------------------------------
#8. Support procedural systemVerilog assertions as if they were
declarative
and contain an antecedent equivalent to the position where they are
located
in the code.
I.e. The simulator should rewrite a given procedural assertion as a
declarative
assertion proceeded by the composition of variables tested by
if/case
statements as an antecedent.
E.g.
always_comb // assert_prob_1
begin
case (next_state)
A: begin
case (theinputs)
I1: if (!thecounter)
begin
theout = these_inputs & these_states;
good_st: assert_strobe ({1;$inset({the_st, the_st2}, 2,
3)}) @@(posedge clk)
else $error("We are doing the wrong thing! state=%h,
inps = %h\n",
state, {in1, in2, in3});
...
This assertion shall be implemented as if it was written as:
always @(posedge clk)
// Run at the end of the timestep (i.e. strobe semantics.)
#(1-) if ( next_state == A // from case statement
&& theinputs == I1 // from the next one.
&& !thecounter // from the it
) assert_strobe ({1;$inset({the_st, the_st2}, 2, 3)})
@@(posedge clk)
else $error("We are doing the wrong thing! state=%h, inps =
%h\n",
state, {in1, in2, in3});
Justification:
The example above may fail falsely due to ordering of the variables
changing.
If next_state changes late in the timestep, the assertion should not
even
be started.
There is a way to ensure that this assertion works correctly. As Harry
points out
the addition of disable good_st at the beginning of the block would
prevent
false firings. E.g.
always_comb // assert_prob_1
begin
disable good_st;
Of course one needs to remember to always add a disable for each
assertion statement
put into a combinatorial block. This may be a ways away from the
actual statement,
and is easily overlooked (in other words, dangerous stuctures.)
This fix though does not allow one to have overlapping assertion
sequences since
the disable statement stops threads of the statement.
Thus, I recommend this requirement to save us from all this headache.
Problems with this requirement:
It makes the implementation a little more difficult.
It is different from SystemVerilog 3.0
--------------------------------------------------------------------------
#9. Extend sugar Verification directives to include optional clocking
specification (to override the presumed global clocking signal.)
Include systemVerilog optional name for directives too. Suggested
syntax includes:
<name> : assert always @(posedge clk) <Expression> ...
Justification:
It appears that a default clock can be specified for subsequent
properties.
I presume that formal tools require the user to define the clock and
properties
use that. Simulation needs to specify the clock a little more
explicitly.
One may want to set a default clock for a module/interface for all
properties.
And one may want to specify a clock on a particular property for only
that
property.
Problems with this requirement:
Optional clock is embedded within the Sugar grammar.
Naming properties/assertions may already be supported by Sugar
(where?)
--------------------------------------------------------------------------
#10. Require the systemVerilog name for directives/properties to be
mandatory.
Justification:
It is good methodology to name properties/assertions/coverage, etc.
The name
provides a symbol to talk about and refer to in discussions/reports,
etc.
Without a name, one is left with a number or a line number. When you
have
many properties in a module, having a name prevents you from looking
at
the wrong property when it fails. Often without a name, people can
find the
wrong assertion/property to review.
Problems with this requirement:
Currently it is optional.
--------------------------------------------------------------------------
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Mon Jul 29 2002 - 03:04:53 PDT