RE: [sv-ac] Re: [SV-AC] Local Variables Flow Out Issue in and/or/intersect/implies

Hi Ben:

I don't see the compelling motivation for this proposal.

property P_illegal;

  int v_t1;

  ((a, v_t1=data) ##1 b) implies // cause, v_t1 can be read in LHS

  (##1 d==v_t1); //effect, v_t1 cannot be read in RHS

endproperty : P_illegal

can be written legally today as

property P_legal;

  int v_t1;

  ((a, v_t1=data) ##1 b) |-> // cause, v_t1 can be read in LHS

  d==v_t1; //effect, v_t1 can be read in RHS

endproperty : P_legal

Similarly,

property P_race;

  automatic int v;

  (a, v=data) ##[1:3] b) implies

  (c==v ##2 d);

endproperty : P_race

can be written legally today as

property P_no_race;

  int v;

  (a, v=data) |->

  (

    (##[1:3] b) implies

    (c==v ##2 d)

  );

endproperty : P_no_race

Best regards,

J.H.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben
cohen
Sent: Thursday, September 02, 2010 2:40 PM
To: sv-ac@eda.org; Korchemny, Dmitry; Eduard Cerny
Subject: [sv-ac] Re: [SV-AC] Local Variables Flow Out Issue in
and/or/intersect/implies

Update the file in http://www.eda-stds.org/svdb/view.php?id=3195
<http://www.eda-stds.org/svdb/view.php?id=3195> , and

Added:
"The local variable shall not be read in the same cycle it is written. "

[Ben] I believe that there would be a race condition because one
property can write a value to the local variable while a concurrent
property reads the property. For example:
property P_race;
  automatic int v;
    (a, v=data) ##[1:3] b) implies
    (c==v ##2 d): // This consequent may be processed before the
antecedent.
endproperty :P_race

On Wed, Sep 1, 2010 at 6:47 PM, ben cohen <hdlcohen@gmail.com
<mailto:hdlcohen@gmail.com> > wrote:

However, there is a need to be able to set and read local variables in
one sequence or property (the LHS), and to read those local variables in
another sequence / property (RHS).

Please see http://www.eda-stds.org/svdb/view.php?id=3195
<http://www.eda-stds.org/svdb/view.php?id=3195>

I uploaded a proposal.

Ben Cohen

-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.