FINAL PROPOSAL, 5-DEC-2003

SVA 3.1A PROPOSAL 11:  RECURSIVE PROPERTY DEFINITIONS
-----------------------------------------------------

DISCUSSION:
-----------

1. General

This proposal extends the SVA language by allowing property
definitions to be recursive.  More generally, several property
definitions may be mutually recursive.

This proposal assumes that the proposals on generalized implication,
property conjunction, property if-else, and property instantiation are
passed.  The last of these enables the use of property instances
within property definitions, thereby opening the possibility of cyclic
dependencies, hence recursive definitions.  This proposal affirms the
legality of recursive definitions with some restrictions.

The kind of recursion created by cyclic dependencies in the property
definitions corresponds to cycles in the transition graphs of automata
built to check the properties.  The recursion does not return and
involves no stack.  The recursion is required to be temporal in the
sense that recursive instances are reached only after a positive
temporal delay.

The primary motivation for allowing recursive properties is to provide
a flexible framework for coding ongoing checkers or coverage monitors
that can deal with complicated assertion requirements, such as those
associated with varying numbers of data beats, out-of-order
completions, retries, etc.


EXAMPLE 1:  Suppose we need to check write data according to the
following conditions:

- Each write operation can have between 1 and 16 
  data beats, and each data beat is 8 bits.

- We have a model of the expected write data that
  is available at acknowledgment of a write request.

- When a write request is acknowledged, it gets a 4-bit
  tag that is used to distinguish data beats for 
  multiple write transactions in flight at the same time.

- Data transfer for a write occurs between 
  address acknowledgment and the last data valid,
  both of which have associated tags to identify the 
  relevant write transaction.

- The data beats for a single write operation occur
  in order.

- At any time after address acknowledgment, but 
  not later than the cycle after the last data valid,
  a write transaction can get the retry signal, which
  has an associated tag to identify the write 
  transaction.  If this happens, then the current 
  data transfer for that write transaction is 
  aborted and the entire data transfer will be repeated.  
  The tag does not change and there is not a new address
  acknowledgment.

- There is no limit on the number of times a write
  transaction can get the retry signal.

While these conditions present a fairly complicated set of temporal
requirements, they are still modest among industrial examples.  They
can be coded in a straightforward way, as shown below, using recursive
property definitions.


   always @(posedge clk)
      assert check_write();
   
   property check_write();
   
      [0:127] expected_data;  // local variable to sample model data
      [3:0] tag;              // local variable to sample tag
   
      disable iff (reset)
      (
         write_request && write_request_ack, 
         expected_data = model_data,
         tag = write_request_ack_tag
      )
      |=> 
      check_write_address_phase(expected_data, tag);
   
   endproperty
   
   property check_write_address_phase
   (
      expected_data, // [0:127] 
      tag            // [3:0] 
   );

      first_match
      (
         ##[0:$] (address_ack && (address_ack_tag == tag))
      )
      |=>
      check_write_data_beat(expected_data, tag, 4'h0);
   
   endproperty
   
   property check_write_data_beat
   (
      expected_data, // [0:127] 
      tag,           // [3:0] 
      i              // [3:0] 
   );
 
      first_match  
      (
         ##[0:$]
         (
            (data_valid && (data_valid_tag == tag))
            ||
            (retry && (retry_tag == tag))
         )
      )
      |->
      (
         (
            (data_valid && (data_valid_tag == tag)
            |-> 
            (data == expected_data[i*8+:8])
         )
         and 
         (
             if (retry && (retry_tag == tag))
                1'b1 |=> check_write_data_beat(tag, expected_data, 4'h0)
             else if (!last_data_valid)
                1'b1 |=> check_write_data_beat(tag, expected_data, i+4'h1)
             else 
                ##1 (retry && (retry_tag == tag))
                |=>
                check_write_data_beat(tag, expected_data, 4'h0)
         )
      );
   
   endproperty


Notice that since there is no limit on the number of times a write
transaction can get the retry signal, the recursion can go on
indefinitely.  This is analogous to the indefinite repetition when
using an LTL "until" operator or the "[*0:$]" unbounded repetition
operator.

////

Recursive property definitions also allow expression of some of
the weak LTL operators without introducing those operators as 
constructs of SVA.  Here are two examples.

EXAMPLE 2 (Always):  If p() is a defined property, then "G p()"
can be achieved by

   property always_p();
      p() and (1'b1 |=> always_p());
   endproperty

Note that SVA already allows attachment of "always" at the 
assertion level.  This recursive definition gives the semantics
of "G p()" in a property that can be instantiated anywhere 
a property can be written [except within the scope of a negation, 
as excluded by Restriction 1 below].
////

EXAMPLE 3 (Weak Until):  If p() and q() are defined properties,
then "p() W q()" can be achieved by

   property p_weak_until_q();
      (q())
      or
      (
         p() and (1'b1 |=> p_weak_until_q())
      );
   endproperty

////


2. Restrictions on Recursive Definitions

The restrictions given here eliminate recursive definitions with
certain pathological semantics and avoid the introduction of 
general liveness properties into SVA.

Defined property p is said to "depend" on defined property q if there
exist n >= 0 and defined properties p_0,...,p_n such that p_0 = p, 
p_n = q, and for all 0 <= i < n, the definition of property p_i
instantiates property p_{i+1}.  In particular, by taking q = p and 
n = 0, it follows that property p depends on property p.

A defined property p has an associated "dependency digraph".  The
nodes of the digraph are all the defined properties on which p
depends.  If q and r are nodes of the digraph, then there is an arc
from q to r for each instance of r in the definition of q.  Such an
arc is labelled by the minimum number of timesteps that are guaranteed
from the beginning of the definition of q until the particular
instance r.  For example, if q is defined by

   property q();
      (a |-> r())
      and
      ((b ##1 c[*0:3]) |=> r());
   endproperty

where a,b,c are boolean expressions, then there is one arc from q to r
labelled by "0" due to "a |-> r()" and there is a second arc from q to
r labelled by "2" due to "(b ##1 c[*0:3]) |=> r()".

A defined property p is called "recursive" if its node appears on a
cycle in the dependency digraph of p.

RESTRICTION 1:  The negation operator "not" cannot be applied to any 
property expression that instantiates a recursive property.  
In particular, the negation of a recursive property cannot be 
asserted or used in defining another property.

RESTRICTION 2:  The abort operator "disable iff" cannot be used in 
the definition of a recursive property.  This restriction is 
consistent with the restriction that "disable iff" cannot be nested.

RESTRICTION 3:  The sum of the arc labels around any cycle of the
dependency digraph of a recursive property must be positive.  In other
words, any recursion must occur after a temporal advance.


3. Implementation Notes

Implementation of recursive properties for simulation checking poses
no conceptual difficulty, since, in principle, checkers for the
various recursive threads can be coded using a programming language
that supports recursion and multi-threading.  For formal verification,
however, a recursive property instance must be compiled into a finite
representation suitable for the formal engines that will be used.  The
static analysis necessary to compile for formal verification can also
significantly improve the performance of simulation checkers for the
recursive property.

The key step in compiling a recursive property instance into a
suitable finite representation is to determine a finite, and hopefully
small, set of instances of recursive properties on which the given
property instance depends.

In order to achieve this step, it must be understood that the bitwidth
of each of the formal arguments to the properties is finite.  Ideally,
these bitwidths would be defined in the property formal arguments, but
property formal arguments in SVA have no types.  Therefore, the
compiler must determine the maximum bitwidth needed for each formal
argument of a recursive property by analyzing its definition and
instances.  Once the bitwidths of the formal arguments are bounded,
there are only finitely many inequivalent actual argument lists for
each recursive property, hence only finitely many inequivalent
instances of the recursive property that are relevant for compilation.
For example, if property p is defined by

   property p(n);
      ((n[0] | n[2]) |-> a)
      and 
      (1'b1 |=> p(n + 1'b1));
   endproperty

then the instance p(x[5:0]) actually gives rise to no more than the
eight instances

   p(x[2:0] + 3'h0), p(x[2:0] + 3'h1), ... , p(x[2:0] + 3'h7)


Once a finite number of instances is obtained, then it should be
possible to generate an appropriate finite representation by linking
partial representations of these instances.  Each such partial
representation consists of a representation of the non-recursive part
of the property instance, just as though the property were
non-recursive, and links or transitions to the partial representation
of a (possibly) different instance to account for the recursion.

In the Extended CBV Statement Semantics proposed to the Accellera FVTC
(3-APR-2002), it was explained in considerable detail how to build
alternating automaton representations of recursive properties in this
way.  See

http://www.eda-twiki.org/vfv/hm/att-0772/01-ecbv_statement_semantics.ps.gz

In practice, of course, the number of inequivalent instances on which
a recursive property instance depends may be prohibitively large.  It
may also be that detection of precise inequivalence is difficult, so
that even if the minimum number of inequivalent instances is
tractable, the computation of such a set from the assertion source is
not.  The LRM will not define precisely what recursive properties must
compile, leaving this as an area in which the implementors can
distinguish themselves.


=======================================================================
PROPOSED LRM CHANGES
=======================================================================


PROPOSED CHANGES TO THE BNF:
----------------------------

   NONE.


PROPOSED CHANGES TO LRM TEXT:
-----------------------------

p. 177, before 17.11.  Add the following Subsection.

      17.10.1  Recursive properties.
      
      SystemVerilog allows recursive property definitions.  A defined
      property is recursive if its declaration involves an instantiation of
      itself.  Recursion provides a flexible framework for coding properties
      to serve as ongoing assumptions, checkers, or coverage monitors.
      
      For example, 
      
         property prop_always(p);
            p and (1'b1 |=> prop_always(p));
         endproperty
      
      is a recursive property that says that the formal argument property p
      must hold at every cycle.  This example is useful if the ongoing
      requirement that property p hold applies after a complicated
      triggering condition encoded in sequence s:
      
         property p1(s,p);
            s |=> prop_always(p);
         endproperty
      
      As another example, the recursive property
      
         property prop_weak_until(p,q);
            q or (p and (1'b1 |=> prop_weak_until(p,q)));
         endproperty
      
      says that formal argument property p must hold at every cycle up to
      but not including the first cycle at which formal argument property
      q holds.  Formal argument property q is not required ever to hold,
      though.  This example is useful if p must hold at every cycle after a 
      complicated triggering condition encoded in sequence s, but the 
      requirement on p is lifted by q:
      
         property p2(s,p,q);
            s |=> prop_weak_until(p,q);
         endproperty
      
      More generally, several property definitions may be mutually
      recursive.  For example
      
         property  check_phase1;
            s1 |-> (phase1_prop and (1'b1 |=> check_phase2));
         endproperty
         property  check_phase2;
            s2 |-> (phase2_prop and (1'b1 |=> check_phase1));
         endproperty
      
      There are three restrictions on recursive property definitions.
      
      RESTRICTION 1:  The negation operator "not" cannot be applied to any 
      property expression that instantiates a recursive property.  
      In particular, the negation of a recursive property cannot be 
      asserted or used in defining another property.
      
      Here are examples of illegal property definitions that violate 
      Restriction 1:
      
         property illegal_recursion_1(p);
            not prop_always(not p);
         endproperty
      
         property illegal_recursion_2(p);
            p and (1'b1 |=> not illegal_recursion_1(p));
         endproperty
      
      RESTRICTION 2:  The abort operator "disable iff" cannot be used in 
      the definition of a recursive property.  This restriction is 
      consistent with the restriction that "disable iff" cannot be nested.
      
      Here is an example of an illegal property definition that violates
      Restriction 2:
      
         property illegal_recursion_3(p);
            disable iff (b)
            p and (1'b1 |=> illegal_recursion_3(p));
         endproperty
      
      The intent of illegal_recursion_3 can be written legally as
      
         property legal_3(p);
            disable iff (b) prop_always(p);
         endproperty
      
      since legal_3 is not a recursive property.
      
      RESTRICTION 3:  If p is a recursive property, then, in the definition
      of p, every instance of p must occur after a positive advance in
      time.  In the case of mutually recursive properties, all recursive
      instances must occur after positive advances in time.
      
      Here is an example of an illegal property definition that violates
      Restriction 3:
      
         property illegal_recursion_4(p);
            p and (1'b1 |-> illegal_recursion_4(p));
         endproperty
      
      If this form were legal, the recursion would be stuck in time, 
      checking p over and over again at the same cycle.
      
      
      Recursive properties can deal with complicated requirements, such as
      those associated with varying numbers of data beats, out-of-order
      completions, retries, etc.  Here is an example of using a recursive
      property to check complicated conditions of this kind.
      
      EXAMPLE:  Suppose that write data must be checked according to the
      following conditions:
      
      - Acknowledgment of a write request is indicated by the signal
        write_request together with write_request_ack.  When a write request
        is acknowledged, it gets a 4-bit tag, indicated by signal
        write_reqest_ack_tag.  The tag is used to distinguish data beats for
        multiple write transactions in flight at the same time.  
      
      - It is understood that distinct write transactions in flight at the
        same time must be given distinct tags.  For simplicity, this
        condition is not a part of what is checked in this example.
      
      - Each write transaction can have between 1 and 16 data beats, and
        each data beat is 8 bits.  There is a model of the expected write
        data that is available at acknowledgment of a write request.  The
        model is a 128 bit vector.  The most significant group of 8 bits
        represents the expected data for the first beat, the next group of 8
        bits represents the expected data for the second beat (if there is a
        second beat), and so forth.
      
      - Data transfer for a write transaction occurs after acknowledgment of
        the write request and, barring retry, ends with the last data beat.
        The data beats for a single write transaction occur in order.
      
      - A data beat is indicated by the data_valid signal together with the
        signal data_valid_tag to determine the relevant write transaction.
        The signal data is valid with data_valid and carries the data for
        that beat.  The data for each beat must be correct according to the
        model of the expected write data.  
      
      - The last data valid is indicated by signal last_data_valid together
        with data_valid and data_valid_tag.  For simplicity, this example
        does not represent the number of data beats and does not check that
        last_data_valid is signaled at the correct beat.
      
      - At any time after acknowledgement of the write request, but not
        later than the cycle after the last data valid, a write transaction
        can be forced to retry.  Retry is indicated by the signal retry
        together with signal retry_tag to identify the relevant write
        transaction.  If a write transaction is forced to retry, then its
        current data transfer is aborted and the entire data transfer must
        be repeated.  The transaction does not re-request and its tag does
        not change.
      
      - There is no limit on the number of times a write transaction can be
        forced to retry.
      
      - A write transaction completes the cycle after the last data valid
        provided it is not forced to retry in that cycle.
      
      
      Here is code to check these conditions:
         
         property check_write;
         
            [0:127] expected_data;  // local variable to sample model data
            [3:0] tag;              // local variable to sample tag
         
            disable iff (reset)
            (
               write_request && write_request_ack, 
               expected_data = model_data,
               tag = write_request_ack_tag
            )
            |=> 
            check_write_data_beat(expected_data, tag, 4'h0);
         
         endproperty
         
         property check_write_data_beat
         (
            expected_data, // [0:127] 
            tag,           // [3:0] 
            i              // [3:0] 
         );
       
            first_match  
            (
               ##[0:$]
               (
                  (data_valid && (data_valid_tag == tag))
                  ||
                  (retry && (retry_tag == tag))
               )
            )
            |->
            (
               (
                  (data_valid && (data_valid_tag == tag)
                  |-> 
                  (data == expected_data[i*8+:8])
               )
               and 
               (
                   if (retry && (retry_tag == tag))
                      1'b1 |=> check_write_data_beat(tag, expected_data, 4'h0)
                   else if (!last_data_valid)
                      1'b1 |=> check_write_data_beat(tag, expected_data, i+4'h1)
                   else 
                      ##1 (retry && (retry_tag == tag))
                      |=>
                      check_write_data_beat(tag, expected_data, 4'h0)
               )
            );
         
         endproperty


PROPOSED CHANGES TO THE FORMAL SEMANTICS:
-----------------------------------------

1. p. 343, G.1.  Change

      b) The abstract syntax eliminates instantiation of sequences and
         properties.  The semantics of an assertion with an instance
         of a sequence or property is the same as the semantics of a
         related assertion obtained by replacing the sequence or
         property instance with an explicitly written sequence or
         property.  The explicit sequence or property is obtained from
         the body of the associated declaration by substituting actual
         arguments for formal arguments.

   to

      b) The abstract syntax eliminates instantiation of sequences and
         properties.  The semantics of an assertion with an instance of
         a sequence or non-recursive property is the same as the
         semantics of a related assertion obtained by replacing the
         sequence or non-recursive property instance with an
         explicitly written sequence or property.  The explicit
         sequence or property is obtained from the body of the
         associated declaration by substituting actual arguments for
         formal arguments.  A separate section defines the semantics
         of instances of recursive properties in terms of the
         semantics of instances of non-recursive properties.


2. p. 343, G.1.  Change

      In order to use this appendix to determine the semantics of a
      SystemVerilog assertion, the assertion must first be transformed
      into an enabling condition together with an assertion in the
      abstract syntax.  This transformation involves eliminating
      sequence and property instances by substitution, eliminating
      local variable declarations, introducing parentheses,
      determining the enabling condition, determining implicit or
      inferred event controls, and eliminating redundant event
      controls.

   to

      In order to use this appendix to determine the semantics of a
      SystemVerilog assertion, the assertion must first be transformed
      into an enabling condition together with an assertion in the
      abstract syntax.  For assertions that do not involve recursive
      properties, this transformation involves eliminating sequence
      and non-recursive property instances by substitution,
      eliminating local variable declarations, introducing
      parentheses, determining the enabling condition, determining
      implicit or inferred event controls, and eliminating redundant
      event controls.


3. p. 344, G.1.  At the end of the section, before G.2, add the following 
   paragraph.

      If the SystemVerilog assertion involves instances of recursive
      properties, then transformation replaces these instances with
      placeholder functions of the actual arguments.  The semantics of
      an instance of a recursive property is defined in terms of
      associated non-recursive properties in Section G.5.  Once the
      semantics of the recursive property instances are understood,
      the placeholder functions are treated as properties with these
      semantics.  Then the ordinary definitions can be applied to the
      transformed assertion in the abstract syntax together with
      placeholder functions.


4. p. 351.  Add the following section to the end of Annex G:

      G.5  Recursive Properties

      This section defines the neutral semantics of instances of
      recursive properties in terms of the neutral semantics of
      instances of non-recursive properties.  The latter can be
      expanded to properties in the abstract syntax by appropriate
      substitutions, and so their semantics is assumed to be
      understood.

      According to Restriction 1 in Section 17.10.1, it is understood
      below that the negation operator "not" cannot be applied to any
      property expression that instantiates a recursive property.
      Restriction 2 in Section 17.10.1 is not represented here because
      "disable iff" is treated as a general property-building operator
      in this appendix.  A precise version of Restriction 3 is given
      below.
      
      Defined property p is said to "depend" on defined property q if
      there exist n >= 0 and defined properties p_0,...,p_n such that
      p_0 = p, p_n = q, and for all 0 <= i < n, the definition of
      property p_i instantiates property p_{i+1}.  In particular, by
      taking q = p and n = 0, it follows that property p depends on
      property p.
      
      A defined property p has an associated "dependency digraph".
      The nodes of the digraph are all the defined properties on which
      p depends.  If q and r are nodes of the digraph, then there is
      an arc from q to r for each instance of r in the definition of
      q.  Such an arc is labelled by the minimum number of timesteps
      that are guaranteed from the beginning of the definition of q
      until the particular instance r.  For example, if q is defined
      by
      
         property q();
            (a |-> r())
            and
            ((b ##1 c[*0:3]) |=> r());
         endproperty
      
      where a,b,c are boolean expressions, then there is one arc from
      q to r labelled by "0" due to "a |-> r()" and there is a second
      arc from q to r labelled by "2" due to "(b ##1 c[*0:3]) |=> r()".
      
      A defined property p is called "recursive" if its node appears
      on a cycle in the dependency digraph of p.  

      The following is a precise version of Restriction 3:
      
      RESTRICTION 3:  The sum of the arc labels around any cycle of the
      dependency digraph of a recursive property must be positive.
      
      Let p(X) be an instance of a recursive defined property p, where
      X denotes the actual arguments of the instance.  For k >= 0, the
      k-fold approximation to p(X), denoted p[k](X), is an instance of
      a non-recursive property p[k] defined inductively as follows.
      
      * The definition of p[0] is obtained from the definition of p by
        replacing the body property_expr with the literal "1'b1".
      
      * For k > 0, the definition of p[k] is obtained from the
        definition of p by replacing each instance of a recursive
        property by its (k-1)-fold approximation.
      
      The semantics of the instance p(X) is then defined as follows.
      For any word w over \Sigma and local variable context L, 
      w,L |= p(X) iff for all k >= 0, w,L |= p[k]