[sv-champions] comments on 1728

From: John Havlicek <john.havlicek_at_.....>
Date: Thu Jul 24 2008 - 07:21:05 PDT
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.
Received on Thu Jul 24 07:22:41 2008

This archive was generated by hypermail 2.1.8 : Thu Jul 24 2008 - 07:22:42 PDT