Subject: Re: Assertion requirements
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Jul 11 2002 - 14:42:30 PDT
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 : Thu Jul 11 2002 - 14:46:26 PDT