Synopsys requirements with explanation
Subject: Synopsys requirements with explanation
From: dudani@us04.synopsys.com
Date: Wed Jul 31 2002 - 13:16:51 PDT
Below are the Synopsys requirements with added explanation and
justification to the ones that were previously submitted. Please also
note that the numbering of items has been corrected.
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.
<step_control> specifies the clock for the assertions. Users may
want to write assertions within a module, or sometimes outside the
module, particularly, for specifying libraries of assertions. When
written within a procedural block, temporal assertions are typically
useful only immediately within an always block or in a nested conditional
block. However, embedding concurrent assertions in a looping block is not
appropriate.
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 (clock)
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). These properties
are forced
to be considered as assertions only.
R2.2:
directive for constraints (i.e. assume). These are forced to be only
assumptions.
Constraints are essential for random simulation, and formal
verification.
R2.3:
directive for use as both assumption and assertion (ie. property). These
properties can be automatically interpreted by tools as assumptions or
asserts,
based on the environment and usage.
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 in synchronous and
asynchronous context.
R4.1:
support for accept on an event expression (i.e. accept). When a reset
occurs
in the middle of a sequence, its corresponding assertion becomes true and
the
evaluation of the sequence is terminated.
R4.2:
support for reject on an event expression (i.e. reject). When a reset
occurs
in the middle of a sequence, its corresponding assertion becomes false
and the
evaluation of the sequence is terminated.
R4.3:
support for asynchronous event expression on R4.1. When an
asynchronous
reset occurs in the middle of a sequence, its corresponding assertion
becomes true
and the evaluation of the sequence is terminated.
R4.4:
support for asynchronous event expression on R4.2. When an
asynchronous
reset occurs in the middle of a sequence, its corresponding assertion
becomes
false and the evaluation of the sequence is terminated.
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). This
allows a user to
terminate further matching on a regular expression when one of the
possible
sequences is already matched.
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. Also, the
results of assertions may vary
- from a simulator to simulator
R8: Intuitive, Easy of use for Verilog design and verification
community
R9: 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
R10: support instantiation of templates with extraction of
context for R1. Restricted to specific
synthesis-like coding styles
for inference of context. The context is derived form the lexical
analysis, such as
clock from the procedural always block, assignment statement (LHS
and RHS)
immediately preceding the assertion, enabling condition etc.
R10.1
extract source context for clock for R11
- R10.2
extract source context for left hand side and right hand side operators
for previous statement
R10.3
extract source context for reset
R10.4
extract source context for enable
R11: Support data checking. It is easy to see that the control part of
the design can be verified
from the sequences of events. However, the data associated with the
events (data and event together normally defined as a transaction) needs
to be verified.
- R11.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. In other words, the sampled values of
design variables is used to update these
- variables.
- R11.2 variables are scope restricted to within assertion block
R11.2
support reference to past data value (i.e. past)
R11.3
support reference to future data value at next cycle (i.e. future)
- R11.4
support concurrent data checking ; per attempt latching of data values to
be checked later within the attempt. Supports data checking on
overlapping sequences
R12: support language features to track coverage of assertion
events
R12.1
coverage for assertions (sequences)
R12.1
coverage sub-sequences within assertions
R12.2
language construct to define time window defined by assertion event. This
would
allow a user to restrict time during which the coverage data is gathered.
R12.3
support naming of coverage items
R12.4
support construction of hierarchy of time_window. A coverage item
can be
gathered within such a nested a sub-time window.
R12.5
support coverage of data values with sampling by assertion events. Data
values
of certain expressions can be examined for coverage at certain events.
R12.6
support coverage of paths within an assertion (sequence) . When
multiple
sequences can be generated from a regular expression, coverage of
various possible sequences (paths) that actually occur can be covered.
R12.7
support feature to combine permutations of coverage items (cross
coverage)
R12.8
support feature to exclude data items or sequence from coverage
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive
Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28
: Wed Jul 31 2002 - 13:19:07 PDT