Subject: Re: Synopsys requirements for SV assertions
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Mon Jul 29 2002 - 07:25:25 PDT
hi surrendra,
below please find comments regarding your proposed requirements:
>R1: support concurrent/declarative form of assertions with event sample
expression (<step_control>) both external to module and internal >to module
in restricted locations within procedural code
first, i'm not sure if i understand what a step_control is (even after
having read the 3.0 specification). it seems to be a mechanism whereby
combinatorial always blocks are made more efficient in simulation by
preventing code from being executed if the specified event does not
evaluate to true. is this correct?
second, i do not understand this requirement. are you suggesting that
assertions should only be allowed in step_control? or that in addition to
everywhere else, they be allowed within step_control? if the latter, then
why mention step_control specifically?
third, when you say "in restricted locations", which restrictions are you
thinking of?
> R2.2: directive for constraints (i.e. assume)
i don't understand this, as i said to rajeev, who had the same requirement.
in order to make this email self-contained, i'll repeat here what i said to
him:
i don't understand what assume would mean in the context of systemverilog:
an assumption in formal verification is used in place of environment
modeling - i.e., when you don't want to explicitly describe the
behavior of the input signals to the design, but rather want to use the
neighboring block's specification as an assumption on the behavior of
the inputs. however, once you are inside of procedural code as in
systemverilog, then presumably you have input behavior. therefore, it
seems there is nothing to assume. what am i missing?
> R2.3: directive for use as both assumption and assertion (ie.
property)
i assume you mean here that a property can be named, then later either
assumed or asserted? if not, then what does this mean?
> R4.2: support for reject on an event expression (i.e. reject)
can you give a real-life example of the use of this?
> R6.1 provide support for matching first sequence (i.e first_match)
same here - can you give a real-life example where you want to match a
sequence rather than a simple boolean expression?
> R7.1 restrict immediate and immediate_strobed assertions to only
allow combinational assertion expressions Motivation: immediate
and immediate_strobed are only applicable to dynamic simulation, and have
no clear semantics for static analysis.
i think what you are saying is that if you have a sequential assertion, you
must clock it? is this a correct interpretation of this requirement? but
the 3.0 spec (top of page 47) says that sequential regular expressions
require a step control event expression (@@). so perhaps i do not
understand what you mean. please clarify.
> R12.1 extract source context for clock for R11 R12.2
extract source context for left hand side and right hand side operators
>for previous statement R12.3 extract source context for reset
> R12.4 extract source context for enable
i don't understand what "extract source context" means.
> R12: Support data checking
also, i don't understand this. can you elaborate?
>R13.1 support declaration, initialization and assignment of variables
within assertion blocks as described in R6.3. Variables are updating
>according to trace semantics of R1.
what are "trace semantics"?
> R14.4 support construction of hierarchy of time_window. A
coverage item can be gathered within such a nested a sub-time >window.
i do not understand this. what is a hierarchy of time_window?
> R14.5 support coverage of data values with sampling by assertion
events
> R14.6 support coverage of paths within an assertion (sequence)
sorry, but these are two more things i do not understand. can you explain?
thanks in advance for your patience.
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
"dudani@us04.synopsys.com" <Surrendra.Dudani@synopsys.com>@eda.org on
25/07/2002 17:56:26
Sent by: owner-assertion@eda.org
To: assertion@eda.org
cc:
Subject: Synopsys requirements for SV assertions
Please ignore if you have already received this mail.
Below are the Synopsys requirements for System Verilog assertions:
System Verilog Assertion Requirements:
R1: support concurrent/declarative form of assertions with event sample
expression (<step_control>) both external to module and internal to module
in restricted locations within procedural code
R1.1: with ability to define sequences with regular expressions
R1.2: ability to define sequences with time windows and time shifts
as # of
sample events
R1.3: ability to define sequences with relationship between events
R1.4: support basic implication operator (i.e. if (bool_expr) then
(seq_expr))
R1.5: support of SystemVerilog <step_control> event (ie. iff)
R1.6: when R1 defined external to module support definition of module and
scope for reference/linking R2: support directives to guide tool
interpretation of assertion intent
R2.1: directive for property assertions (i.e. check, forbid)
R2.2: directive for constraints (i.e. assume)
R2.3: directive for use as both assumption and assertion (ie.
property)
R3: support synchronous clocking for R1
R3.1: ability to define sample expression as a boolean expression
of design signals
R3.2: ability to define multiple clocks, and synchronization
between
clocks(i.e. ended and matched)
R4: support set/reset of assertions for R1
R4.1: support for accept on an event expression (i.e. accept)
R4.2: support for reject on an event expression (i.e. reject)
R4.3: support for asynchronous event expression on R4.1
R4.4: support for asynchronous event expression on R4.2
R5: support mechanism for defining and instantiating pre-built generic
assertions
(i.e template definition and instantiation feature for assertions)
The purpose here is to be able to express generic assertions with
parameters as input and then feature to instantiate in the design. This
capability would be similar to macros in C in that they are immediately
in-lined at compile time and do not result in module hierarchy.
R6: Support useful productivity and expressiveness features
R6.1 provide support for matching first sequence (i.e first_match)
R6.2 provide support for restricting length of a sequence (i.e.
length) R6.2 provide support for asserting that sequences should
hold true for duration of time window (i.e. istrue) R6.3 provide
block concept to group assertion statements Provide syntax sugar
to group assertions and share common <step_control> and accept/reject
conditions across all assertions within block. Block would also contain
variable declarations whose scope would be local to block. Blocks can also
be named. R6.4 support features to express sets, and operator on sets such
as mutual exclusiveness, membership, non-membership, union, intersection
and difference
R7: Clearly delineate immediate assertions from clocked assertions
R7.1 restrict immediate and immediate_strobed assertions to only allow
combinational assertion expressions Motivation: immediate and
immediate_strobed are only applicable to dynamic simulation, and have no
clear semantics for static analysis.
R9: Intuitive, Easy of use for Verilog design and verification community
R10: support R1 in-lined within restricted areas of procedural
SystemVerilog code R10.1: restrict to only top level within always block,
in other words not embedded in while, repeat loops or non-clocked
(re-entrant) always blocks R11: support instantiation of templates with
extraction of context for R1. Restricted to specific synthesis-like
coding styles for inference of context.
R12.1 extract source context for clock for R11 R12.2
extract source context for left hand side and right hand side operators for
previous statement R12.3 extract source context for reset
R12.4 extract source context for enable
R12: Support data checking R13.1 support declaration,
initialization and assignment of variables within assertion blocks as
described in R6.3. Variables are updating according to trace semantics of
R1. R13.2 variables are scope restricted to within assertion block
R13.2 support reference to past data value (i.e. past)
R13.3 support reference to future data value at next cycle (i.e.
future) R13.4 support concurrent data checking ; per attempt
latching of data values to be checked later within the attempt. Supports
data checking on overlapping sequences R13: support language features to
track coverage of assertion events
R14.1 coverage for assertions (sequences)
R14.1 coverage sub-sequences within assertions
R14.2 language construct to define time window defined by assertion
event
R14.3 support naming of coverage items
R14.4 support construction of hierarchy of time_window. A coverage
item can be gathered within such a nested a sub-time window.
R14.5 support coverage of data values with sampling by assertion
events
R14.6 support coverage of paths within an assertion (sequence)
R14.7 support feature to combine permutations of coverage items
(cross coverage)
R14.8 support feature to exclude data items or sequence from
coverage
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
154 Crane Meadow Road
Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Mon Jul 29 2002 - 07:26:19 PDT