Subject: Re: Assertion requirements
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Jul 31 2002 - 05:50:13 PDT
adam,
>Problems with this requirement:
>Is there a reason Sugar does not support this?
no, there is no reason, and i've already proposed to the fvtc committee to
make a small change to sugar such that this is supported (except that i
don't believe an enable is needed. enabling should come from the clock
signal, so that prev(bus[3],5)@clk should give you the value of bus[3] 5
clocks ago).
>It appears that the 'next' operator could be used to compare
>the current value against the next value.
>
> E.g. addr[31:0] == next addr;
>
> But it is not clear...
no. next() cannot be clocked. next gives you the value at the very next
tick of time, without the ability to clock it. it is useful primarily for
sophisticated modeling of environments in formal verification.
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 24/07/2002 21:26:24
Sent by: owner-assertion@eda.org
To:
cc: Adam Krolnik <krolnik@lsil.com>, assertion@eda.org, sv-ac@eda.org
Subject: Re: Assertion requirements
Good afternoon;
I would like to modify my requirements given a greater understanding
of Sugar 2.0. Please replace the previous #5 requirement with this new
versions.
--------------------------------------------------------------------------
#5 Support a functional method to access past state.
The word 'functional' implies function like as opposed to
a separate procedural method. This method should provide the
ability to return the value of a vector from 1 or more cycles
in the past. This method should utilize the base clock of an
assertion
or any specific clock associated with the method. The method should
also support gated (by an explicit signal) clocks. This explicit
signal would indicate if the value would be transferred to the
next cycle (much as like an enabled FF would transfer its
current value to the next cycle when enabled.) E.g. I am trying
to provide a model for the following RTL code of a gated clock
register:
always @(posedge clk)
begin
if (clken) q <= d;
end
Here is an example of a function and its (recursive) definition:
prev(expr, N, en)
- expr is expression (1 or more bits) to produce value for.
- N is the number of previous cycles to get value from.
- en is an enable for the previous cycle's clock. If true
next cycle has new value, otherwise need to go to
next previous cycle.
Definition:
prev(expr) :== <previous cycle value of expr>
prev(expr, 0),
prev(expr, 0, en) :== expr
prev(expr, N) :== prev(prev(expr, N-1))
prev(expr, N, en) :==
prev(en) ? prev(prev(expr, N-1, en))
: prev(prev(expr, N, en));
Justification:
It is common to utilize past signal values to check for proper
operations.
Sequences allow specification of a combination of values throughout
time,
but does not allow one to utilize a past value in the current time.
For
example, one may wish to know the past value of a fifo pointer to
make a comparison with the current value.
E.g. fifo_ptr = previous(fifo_ptr) + 1;
This method should allow access to previous values from multiple
cycles
ago. This is syntactic sugar for previous(previous(expr)), etc. This
will
add no new definitions, yet make maintenance and creation of
assertions
easier.
This method should support an explicit signal to define when a
previous
cycle actually occurred. For designs with gated clocks (logic that
determines whether or not a register will update with the current
value.)
the enable will allow the assertion writer to follow the design,
ignoring cycles when registers (logic) don't update their values.
Without this explicit signal, one has to synthesize their own
definition.
Without recursive macro definitions, the support is limited to only
a few clocks.
Without past value capabilities, there is reluctance to write an
assertion
because one has to provide code (only for simulation or formal) to
create this state. This state may occur and can simply be used, but
may
also disappear with code optimization. If the user is writing an
assertion
in a procedural codeset, they must create some code away from the
actual
code in question. E.g.
if (this) if (that) case (other) a: begin if (again) assert (...);
// Oh no, I need the value of signal foo222 from 2 cycles ago. I
// do not need that signal though for the design... Okay what do I
// need to do?
...
end
// Hopefully not 100s of lines later...
//synopsys translate_off
// Only for assertion blah, blah, blah
reg [3:0] foo222_dly2, foo222_dly1;
alway @(posedge clk or negedge rst_n)
begin
if (!rst_n) {foo222_dly2, foo222_dly1} <= {4'b0, 4'b0};
else
{foo222_dly2, foo222_dly1} <= {foo222_dly1, foo222};
end
//synopsys translate_on
This capability has the ability to reduce the number of instances
where
a forall expansion is needed. If you can access past state for
comparison
later, you do not need to spawn several assertions with each data
value
to compare later.
Problems with this requirement:
Is there a reason Sugar does not support this?
It appears that the 'next' operator could be used to compare
the current value against the next value.
E.g. addr[31:0] == next addr;
But it is not clear...
The definition for previous is complex if you take into account
the support for enables on gated clocks.
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Original proposal:
===========================================================================
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 : Wed Jul 31 2002 - 05:51:06 PDT