Group I Issues

Discussion

Note that Issue 16 should be included here even though it was rejected, because it is related to the other issues.

For issue 36 (clarifying whether 'replication' is required), the Extensions SC decided that the LRM should make it clear that an implementation need not actually replicate (i.e., make multiple copies of) a property contained within a forall construct. It was mentioned that the LRM used to have a note to this effect, and that the note should be restored.

For issue 41 (generalization of forall to allow it to apply to sub-properties), we first discussed the need for this. It was mentioned that you can't always move forall out to the top level of the property, e.g. when if appears on the LHS of an implication. We then discussed the notion of defining a "for some" construct that would essentially be the dual of forall, involving disjunction instead of conjunction, and potential uses of such a construct for both properties and sequences. However, the need to define negation on sequences in order to define the duality relationship seemed to make this impossible. As an alternative, we considered using the existing AND and OR operators with replication parameters, which would the issue of negation on sequences. An example might be something like

&& [i in {1:10}] (a[i] -> b[i])

or

|| [i in {1:10}] (a[i] -> b[i])

For issue 25 (applying forall to directives), we noted that this would seem to require actual replication (i.e., creation of separate directives) rather than conjunction, since conjunction is a logical operation that doesn't apply to directives. We noted that, intuitively, the user would expect forall outside a property to mean replication, whereas inside should be conjunction. We also noted that using parameterized AND, OR operators for conjunction or disjunction inside a property would allow us to use forall outside a property to actually mean replication (contrary to decisions made regarding issue 36). However, the SC felt that the proposal to define new parameterized AND/OR operators should be treated as a new and separate issue, to be considered for the second release.

Ultimately we decided that in the first release, we should consider only removing the restriction that prohibits use of forall below the top level of a property. Parameterized AND/OR operators would be considered in the second release. As for forall applied to directives, the SC could not identify any clear reason for doing so, and agreed to not pursue the issue further. (However, after the meeting, an example was posted to the web giving a reason why forall applied to directives would be useful.)

(Initial) Resolution

1. The 'illegal' example (pg 81, lines 49-51) should be moved to the "legal" section.
2. On pg 80, line 37, change note to say "is considered statically computable" rather than "is considered to be a static variable".
3. Add a note to the effect that "The term 'replicated property' does not imply that an implementation must provide this functionality by actually replicating; rather, more efficient implementations that provide the same functionality without explicitly replicating are allowed."
4. Specify the VHDL type of each form of replicator variable, in a VHDL context
   • forall i in Boolean => Std.Boolean
   • forall i[..] in Boolean std_ulogic_vector
   • forall i in [..] Std.Integer
   • forall i[..] in {...} => Undefined in the PSL LRM, but note that an implementation might use any array of type Integer - analogous to concatenation results as defined in the VHDL LRM
5. change "replicated to ..." to "is equivalent to f(True) && f(False) ..."
6. consider removing restriction that prohibits use of forall below the top level of a property
7. add an issue regarding the need for parameterized AND/OR operators to provide conjunction or disjunction of instances of a property or sequence over the range of values of the parameter.
8. do not use 'forall' for two different meanings

Additional Notes

• Steve Bailey provided an example for why 'forall' applied to directives would be useful:

  We do need to support forall capability at the directive level.  
  After the meeting, it hit me that this is how we add basic bin 
  coverage to PSL.  For example, to know how many times each state 
  in an FSM has been hit:
  
    type FSM_State is (S0, S1, S2, S3, S4); 
    signal current_state : FSM_State; 
  
    -- psl default clock is rose(clk); 
    -- psl forall State in [S0 to S4] : cover current_state = State; 
  
  Forgive any syntax errors. 
  
  The point being that you don't want the sum of cover S0 + cover S1 
  + cover S2 + cover S3 + cover S4 recorded and reported.  You want 
  each cover recorded and reported separately.  Assuming the forall-
  type capability at the directive level is replication, then you get 
  separate coverage bins for each sequence (state in the example).  
  Otherwise, the user must write each cover explicitly and separately 
  (even with parameterized sequences this is very cumbersome and not 
  user-friendly).
  

Further Discussion (30 Nov 04)

Sitvanit noted that, if we allow forall operators to be nested, then we must define the precedence of forall operators w.r.t. the other operators. Sitvanit proposed two alternatives:

1. Give forall higher precedence than the boolean connectives (and, or, not), as in first order logic.
2. Give forall lower precedence than HDL operators (including HDL and, or, not), but higher than the rest.

Cindy pointed out that option 1 would split the HDL operators into two groups - those with higher precedence than forall (e.g., equality) and those with lower precedence (and, or, not).

Erich suggested a third alternative: give forall lowest precedence. This would be backward compatible with the current syntax (where forall is at the outermost level, and therefore binds last), and it would allow nested foralls provided that parentheses are used.

Further Resolution (30 Nov 04)

1. Define precedence of forall as lower than always
2. Add a note that this implies that a nested forall requires parentheses around the property
3. Be aware that this may impact Issue 50 w.r.t. any equivalence relationships we define

Even Further Discussion (7 Dec 04)

Dana pointed out that Issue 50 (parameterized 'reduction' AND/OR operators) should really be part of this discussion. If we implement those operators, then we will have two operators for the same thing - forall, and parameterized AND. Also, if we implement parameterized operators, then the 'forall' keyword could be used for replication at the directive level.

The possibility of using %for at the directive level was raised. Tej pointed out that %for is a compile-time operator, hence it requires compile-time static expressions; whereas forall only requires elaboration-time static expressions and is therefore more flexible.

We agreed that we should consider issue 50 at the same time as any changes to forall, because we should not have the same keyword meaning different things. If we were to use forall for directives (for cover directives in particular), and parameterized 'reduction' AND/OR operators for properties, then this would not be backward compatible with PSL v1.1. However, there are other areas where we have not maintained backward compatibility, and it can be argued that it is better to break backward compatibility now, with the first IEEE standard, then later.

Even Further Resolution (7 Dec 04)

1. We will develop all three proposals in parallel and then evaluate them
2. Avigail and Sitvanit will detail the changes required to simply relax the restriction that prohibits nested forall, including defining the precedence of forall.
3. Dana will detail the changes required to add parameterized 'reduction' AND/OR operators that would subsume the current forall capability (with parameterized AND for properties) as well as add new capability (parameterized OR for properties, and also parameterized &&/&/| for sequences).
4. Tej will detail the changes required to apply forall to the directive level.

Note also that issue 47 (typed forall variables) has been added to this group, the resolution of which may influence the above-mentioned proposals.

Final Resolution (21, 28 Dec 04)

1. We agreed to adopt parameterized and/or operators.
2. We will keep forall for a while, for backward compatibility.
3. We will relax SS restriction on && on properties to allow non-Boolean LHS (and later, we decided to relax RHS too).
4. We agreed to allow the modeling layer to embed directives in HDL generate statements (for 'forall on directives').
5. We agreed to define the scope of the parameter to extend to the end of the 'for' property or sequence.

LRM Change Proposals

1. Clarification and Relaxation of Forall restrictions (Avigail, Sitvanit)
2. Addition of Parameterized AND/OR Operators (Dana)
3. Application of Forall to Directives (Tej)

LRM Changes

1. First Draft
2. Second Draft

• The grammar may need further coordination with what exists already for forall (or vice versa).
• We still need to propose changes that will allow directives within HDL generate statements.
• The latest proposal seems to need refinement to specify/limit the scope of the 'for' variable.
• We need to coordinate this change with others that will affect the Simple Subset and the structure of section 6.