RE: [sv-champions] comments on 1728

Hi John,

I've never tried to prove it formally, it is OK with me to omit this
statement :).

Dmitry

-----Original Message-----
From: owner-sv-champions@server.eda.org
[mailto:owner-sv-champions@server.eda.org] On Behalf Of John Havlicek
Sent: Friday, July 25, 2008 5:54 PM
To: Korchemny, Dmitry
Cc: john.havlicek@freescale.com; sv-champions@server.eda.org
Subject: 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.

---------------------------------------------------------------------
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.