[sv-ac] 3195: Local Variables Flow Out Issue in and/or/intersect/implies // Updates

http://www.eda-stds.org/svdb/view.php?id=3195
Major updates. The following represents the key element of this proposal.
16.10.1 const local variable
Local variables declared in properties can be qualified as const. The
following describes the rules in using such variables.
Update rules of const local variables
1) Local variables qualified with the keyword const can only be updated in
the antecedent of an implies or implication operators (i.e., |->, |=>). It
shall be illegal to update such variables in the consequent.
2) During any one cycle, the update shall be singly (i.e., the local
variables cannot be updated in the same cycle across the and, or, or
intersect operators) . Thus, the following is illegal:
   P_illegal;
     const int v;
     (a, v=1) and (c, v=2) implies (d && e==v); //Illegal
 endproperty

Read rules of const local variables
1) Within an antecedent, it shall be illegal for a const local variable to
be read in the same cycle within the branching expressions like implies, and
, or, and intersect. Thus, the following is illegal:
  P_illegal2;
     const int v;
     (a, v=1) and (c==v) implies (d); //Illegal
 endproperty

2) Within the consequent, the const local variable can be read at any cycle,
including the cycle in which the variable is updated, within the branching
expressions like implies, and, or, and intersect. Thus, local assertion
variables declared as const flow through from antecedent to consequent at
any cycle, including the current cycle. That means that at any cycle, the
antecedent is always computed first before the consequent. For example:

    property P2;
     const int v1;
       (a, v1=b) and // time step 0
       ((##1 c, v1=v1+1)[*2]) // time step 1 and 2
         implies // could use |-> , |=>
         ((d && e==v1) and // time step 0
         (##[1:2] f==v1)) or // time step 1 and 2
         (##3 f); // // time step 3
  endproperty : P

Note: the application of the implies operator enables the definition of
antecedent and consequent to start at the same time step. This is unlike
the implication operators where the antecedent must complete before the
consequent start.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.