Synopsys requirements for SV assertions

Subject: Synopsys requirements for SV assertions
From: dudani@us04.synopsys.com
Date: Thu Jul 25 2002 - 07:56:26 PDT

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 : Thu Jul 25 2002 - 08:03:35 PDT