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 >> >> > > >Received on Fri Jul 14 06:48:08 2006
This archive was generated by hypermail 2.1.8 : Fri Jul 14 2006 - 06:48:17 PDT