[sv-bc] Re: [sv-ec] [sv-ac] 1549 and inside operator

Hi Dmitry:

I think that your example

   sequence s(x, y);
      ##1 x inside {y};
   endsequence

   assert property(@clk  s(a, '{1,3,5}));

will be illegal under the current description of the rewriting 
algorithm in 1549 provided that

   a inside {'{1,3,5}}

is illegal.  

I prefer not to add any special note about this in 1549.

One could add language to 10.8 as Gord suggested in a later mail, 
but that should be a separate Mantis item.

J.H.

> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.21,255,1188802800"; 
>    d="scan'208";a="243795517"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Wed, 10 Oct 2007 18:57:30 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ec] [sv-ac] 1549 and inside operator
> Thread-Index: AcgLXe6r95DRpKxUS/2abHKe61kdJAAAFXlQ
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda.org>, <sv-bc@eda.org>, <sv-ec@eda.org>
> X-OriginalArrivalTime: 10 Oct 2007 16:57:34.0916 (UTC) FILETIME=[A7BE5840:01C80B5E]
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-eda.org-MailScanner-SpamScore: ss
> X-Spam-Status: No, No
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org id l9AH3e4F026953
> Sender: owner-sv-ac@eda.org
> X-eda.org-MailScanner-Information: Please contact the ISP for more information
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> 
> I agree, there are many issues here. I think that at the very least
> there should be a note in the LRM that this construct is illegal in the
> untyped context, but I would like to find some satisfactory solution (if
> it exists).
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: Gordon Vreugdenhil [mailto:gordonv@model.com] 
> Sent: Wednesday, October 10, 2007 6:51 PM
> To: Korchemny, Dmitry
> Cc: sv-ac@server.eda.org; sv-bc@server.eda.org; sv-ec@server.eda.org
> Subject: Re: [sv-ec] [sv-ac] 1549 and inside operator
> 
> Korchemny, Dmitry wrote:
> > Maybe the problem is in the vague definition of 'inside' operator?
> > Essentially it requires an argument list as its second argument, but
> SV
> > does not have such a construct.
> 
> That isn't the only issue.
> 
> For an aggregate (a '{}) one needs a type context in order to
> determine the type of the elements.  Since the type cannot
> be inferred here, we cannot determine the sizing, sign, etc.
> of even integral terms.  If you attempt to make this all
> self-determined, you will not in general end up with a
> homogenous type and will cause problems elsewhere in the
> language.
> 
> Gord.
> 
> 
> 
> > 
> > Thanks,
> > Dmitry
> > 
> > -----Original Message-----
> > From: Gordon Vreugdenhil [mailto:gordonv@model.com] 
> > Sent: Wednesday, October 10, 2007 6:33 PM
> > To: Korchemny, Dmitry
> > Cc: sv-ac@server.eda.org; sv-bc@server.eda.org; sv-ec@server.eda.org
> > Subject: Re: [sv-ec] [sv-ac] 1549 and inside operator
> > 
> > 
> > 
> > Since "x" and "y" are untyped, I don't know what to do with
> > the `{1, 3, 5} form.  There is no type that I can appeal to
> > in order to determine what to produce.
> > 
> > So I don't think that what you have is valid at all.
> > 
> > I guess that you could have:
> >     typedef int arr[$];
> > 
> >    ...   s(a, arr'('{1,3, 5}))
> > 
> > but I don't think you can use the '{} form with an
> > untyped formal and have the type be inferred.
> > 
> > Gord.
> > 
> > 
> > Korchemny, Dmitry wrote:
> >> Hi all,
> >>
> >>  
> >>
> >> I have the following use case that is directly (or indirectly)
> related
> > 
> >> to 1549 resolution. Consider the following sequence:
> >>
> >>  
> >>
> >> sequence s(x, y);
> >>
> >> ##1 x inside {y};
> >>
> >> endsequence
> >>
> >>  
> >>
> >> What is the right way to pass a set to this sequence instantiation in
> > a 
> >> concurrent assertion? Should it be
> >>
> >>  
> >>
> >> assert property(@clk  s(a, '{1,3, 5});
> >>
> >>  
> >>
> >> ?
> >>
> >>  
> >>
> >> Or should other (which) syntax be used?
> >>
> >>  
> >>
> >> It looks like the LRM does not define it precisely.
> >>
> >>  
> >>
> >> Thanks,
> >>
> >> Dmitry
> >>
> >> ---------------------------------------------------------------------
> >> Intel Israel (74) Limited
> >>
> >> This e-mail and any attachments may contain confidential material for
> >> the sole use of the intended recipient(s). Any review or distribution
> >> by others is strictly prohibited. If you are not the intended
> >> recipient, please contact the sender and delete all copies.
> >>
> >>
> >> -- 
> >> This message has been scanned for viruses and
> >> dangerous content by *MailScanner* <http://www.mailscanner.info/>,
> and
> > is
> >> believed to be clean.
> > 
> 
> -- 
> --------------------------------------------------------------------
> Gordon Vreugdenhil                                503-685-0808
> Model Technology (Mentor Graphics)                gordonv@model.com
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 
> 

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