[sv-ac] RE: sv-ac 1531

But figuring out all the cases that may  or may not be legal need not be
easy. 
Yet, such a static variable is useful when used with caution. Could we
just state that if there is a point in time when a non-deterministic
choice arises (a WAW, RAW/WAR hazard) then the property is illegal?
Without having to enumerate the possible cases?

ed


> -----Original Message-----
> From: Doron Bustan [mailto:dbustan@freescale.com] 
> Sent: Friday, July 14, 2006 9:48 AM
> To: Eduard Cerny
> Cc: sv-ac@eda-stds.org
> Subject: Re: sv-ac 1531
> 
>  From practical point of view I don't think that it should be 
> possible 
> for two
> different tools to give different results for the same pure SVA 
> assertion. If you choose
> to use tasks to create side affects, that should be at your own risk.
> 
>  From theoretical point of view, for every assertion A and 
> computation W
> there should be a clear status of whether the computation 
> satisfies the 
> property.
> There is a refinement for weak and strong satisfaction, but 
> that is also 
> deterministic.
> This definition should be used in simulation, formal, emulation etc.
> 
> Doron
> 
> Eduard Cerny wrote:
> 
> >Doron,
> >
> >I would be for leaving the semantics as loose as possible, in other
> >words, if the user writes to a global variable from two parallel
> >processes, there is nothing in the language to stop him/her. 
> Why do we
> >have to policy it in the assertios? As I said earlier, if I 
> use tasks, I
> >can do this today, but it is cumbersome. 
> >
> >ed
> > 
> >
> >  
> >
> >>-----Original Message-----
> >>From: Doron Bustan [mailto:dbustan@freescale.com] 
> >>Sent: Thursday, July 13, 2006 6:27 PM
> >>To: Eduard Cerny
> >>Cc: sv-ac@eda-stds.org
> >>Subject: sv-ac 1531
> >>
> >>Ed,
> >>
> >>we need a  definition of a semantic for static local variables.
> >>In particular it make sense to define different flow rules
> >>for static local variables.
> >>
> >>for example
> >>
> >>property p1;
> >>logic [3:0] v;
> >>
> >>((a, v = 1) or (b, v=2)) ##1 (v == 1);
> >>endproperty
> >>
> >>is legal, but
> >>
> >>property p2;
> >>static logic [3:0] v;
> >>
> >>((a, v = 1) or (b, v=2)) ##1 (v == 1);
> >>endproperty
> >>
> >>probably should not be legal, because the value of v flowing 
> >>out of ((a, 
> >>v = 1) or (b, v=2)) is undefined.
> >>
> >>BTW, I think that initialization should be in a separate proposal.
> >>
> >>Doron
> >>    
> >>
> >
> >  
> >
> 
>