[sv-ac] 3195:Local Variables Flow Out...// Moved to drop the proposal

I added the following note at http://www.eda-stds.org/svdb/view.php?id=3195
June 28 discussion revealed that there are several issues with this
proposal, and the current use of checkers resolved the requirements for
formal verification, but not for simulation.
Given issues caused by this proposal, I move that this 3195 mantis be
dropped from further consideration.
Ben Cohen

*Today's meeting notes
*
*3195:Local Variables Flow Out Issue in and/or/intersect/implies
       (Ben) (Reviewed by Scott, Dana)
Ben: Has uploaded a proposal for this item, and Scott has reviewed it.
Erik: Find this example compelling.
Ben: Example in proposal: uses "implies" , which is equivalent to
       not (a) or (b), where a, b can be properties.
       Consequent of implies can start evaluating before antecedant
       completes.
       As opposed to |-> |=> operators, where antecedant completse before
       consequent begins evaluation
       Proposal would require evaluation of antecedant first at any clock
       tick, and then "flow" the variables to the consequent for evaluation
       on that clock tick or any following clock tick.

Dana: You are trying to impose an order on an operator which is not
ordered.
Dana: What you want is the semantics of PSL "forall"
Dana: You have that semantics for PSL "forall" by using constant rand
       when using formal verification.
       The problem is that for simulation, the semantics for constant rand
       checker variables do not give you the semantics of PSL forall.
       The question is how to define the semantics for simulation so that it
       implements the forall semantics.
Jacob: Also, since arguments of "implies" are properties. They evaluate to
       true at time 0. This change would result in changes to rewriting
       rules.
Ben: Looks like this proposal should be dropped.*

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