RE: [sv-champions] comments on 1728

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:
  
        let at_least_two(sig, rst = 1'b0) = rst || ($countones(sig) >=
2);
        logic [15:0] sig1;
        logic [3:0] sig2;
     
        always_comb begin
           q1: assert (at_least_two(sig1));
           q2: assert (at_least_two(~sig2));
        end
     
     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.
  
  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}.
  
  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:
  
     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).
  
  This text appears in other places in discussing sequence and property
  arguments.
  
  I recall that Gord raised some concern about misinterpreting this to
  mean that the actual is first reduced to self-determined result type 
  and that is then cast to the type of the formal.  
  
  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.


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