Re: [sv-champions] comments on 1728

Hi Dmitry:

My intuition is in agreement with you, but making precise the
notion of "it cannot be generic" is not something I think we
should be spending time on right now.

If you already have this formalized and proved, then you could
add it back in with a statement like "it can be proved that
<add here your precise rendering of "it cannot be generic">". 

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.31,250,1215414000"; 
>    d="scan'208";a="600802439"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Fri, 25 Jul 2008 07:24:40 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-champions] comments on 1728
> Thread-Index: AcjtmR0eNYLZiOdTRpKc5XVB8gHqOQAcgo9Q
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 25 Jul 2008 04:25:09.0607 (UTC) FILETIME=[6C6C9F70:01C8EE0E]
> 
> Hi John,
> 
> Sure, for this specific example a function may be written, but it cannot
> be generic. In any case, I removed this note, let's see if the people
> agree.
> 
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-champions@server.eda.org
> [mailto:owner-sv-champions@server.eda.org] On Behalf Of John Havlicek
> Sent: Thursday, July 24, 2008 5:21 PM
> To: sv-champions@server.eda.org
> Subject: [sv-champions] comments on 1728
> 
> My comments on 1728 are below.
> 
> J.H.
> 
> * On p. 4:
>  =20
>         let at_least_two(sig, rst =3D 1'b0) =3D rst || ($countones(sig) >=
> =3D
> 2);
>         logic [15:0] sig1;
>         logic [3:0] sig2;
>     =20
>         always_comb begin
>            q1: assert (at_least_two(sig1));
>            q2: assert (at_least_two(~sig2));
>         end
>     =20
>      In this case the let instantiation cannot be replaced by a function
>      call since formal arguments of a function need to have a specific
>      type.
>  =20
>   Is it true that calls to a (single) function cannot replace the calls
>   shown to this let?  Suppose that the function took logic[15:0] on the
>   sig formal.  Do the rules of passing ~sig2 to sig extend ~sig2 by 0 or
>   by its high order bit?  Even if ~sig2 were extended by its high order
>   bit, the actual could be changed to {12'b0,~sig2}.
>  =20
>   I don't think that it is important to try to demonstrate the
> superiority
>   of let in the LRM.  If it is to be done, then the wording should be
> more
>   precise and the argument given more carefully.  For a given model, it
>   might be possible to examine all the calls to a let and determine a
> way
>   to uniformize a function to handle them all.  By using mechanisms to
>   examine bitwidths and types, there might be clever ways to do this.
> 
>   My opinion is that there is no need to put this kind of apology for
>   let in the LRM.
> 
> * On p. 4:
>  =20
>      Otherwise, the self-determined result type of the actual argument
> shall
>      be cast compatible (see 6.22.4) with the type of the formal
>      argument. The actual argument shall be cast to the type of the
> formal
>      argument before being substituted for a reference to the formal
> argument
>      in the rewriting algorithm (see F.5.2).
>  =20
>   This text appears in other places in discussing sequence and property
>   arguments.
>  =20
>   I recall that Gord raised some concern about misinterpreting this to
>   mean that the actual is first reduced to self-determined result type=20
>   and that is then cast to the type of the formal. =20
>  =20
>   This is not what the text actually says, but if SV-SC changed the text
> 
>   in the other places, then this instance should be aligned.
> 
> 
> --=20
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 
> ---------------------------------------------------------------------
> 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.