RE: [sv-bc] Re: [sv-ec] Updated proposal for 'let' syntax

Hi Gord,

I would like to preface my answers with one general observation: our
intention was not to vote for this mantis in SV-AC, but to vote for its
motion to SV-BC. Even if the proposal is not mature enough, I believe
that this is the right thing to do, and your comments are the best
proof: in SV-BC and SV-EC the people have much more relevant expertise,
and they may point out to many potential problems with this proposal
which would escape from SV-AC people, and also to suggest more general
solutions.

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ec@server.eda.org [mailto:owner-sv-ec@server.eda.org] On
Behalf Of Gordon Vreugdenhil
Sent: Saturday, June 09, 2007 12:58 AM
To: Mark Hartoog
Cc: sv-ac@server.eda.org; sv-bc@server.eda.org; sv-ec@server.eda.org
Subject: Re: [sv-bc] Re: [sv-ec] Updated proposal for 'let' syntax


Mark and all,

The "let" construct is somewhere between a macro and a
function.  Allowing such a construct to participate
arbitrarily through hierarchical references throughout
the design is very troublesome.

I have no substantial objection to "let" as an imported
item from a package, nor to direct references to "let"
in a local context.  There are still some issues, but
I think they are resolvable.

I do have numerous problems with "let" in fully general
hierarchical contexts.

It is not clear to me that "let" would lose critical
functionality if references were restricted to being
non-hierarchical in nature.  Perhaps someone from AC
could comment on real use case issues in such contexts.

Your working definition of "let" expansion following
elaboration is extremely problematic from a large scale
design standpoint.  If one has very large sections of
code that are separately compiled (in some vendor library)
for which source is no longer available, it seems
that a necessary restriction of implementations would
be that hierarchical references to such "let" declarations
would not be permitted.  Such restrictions would ensure
that no implementation is fully LRM compliant and that
in real flows what users could expect to work would
vary in an implementation dependent manner.  Is that
really a direction that everyone wants to follow?

I understand that this problem already exists in the context
of assertions constructs.  I view "let" as being much
more troublesome because it can interact with non-asssertions
contexts in widely different ways.  It may be acceptable
in an assertions context to have a somewhat restrictive
model for implementation, but I am very concerned about
such assumptions leak out into the general language.  These
assumptions, if encoded, can have a substantial impact
on vendor models for separate compilation and how robust
and flexible such models are over the language in general.

[Korchemny, Dmitry] The main reason why the hierarchical references to
"let" were included into the proposal was the desire to keep the "let"
definition aligned with the definition of sequences and properties.
Another reason was to use it for multiple argument handling, as
illustrated by the following motivation example from the proposal:

int args[50:1];
for (genvar i = 0; i <= 50; i++) begin : b1
     if (i == 0) begin : b2
        let res = '0;
     end
     else begin : b2
     let res = b1[i-1].res + args[i];
     end
 end
 let res = b1[50].b2.res;

(here the idea is shown for an array, but the same principle can work
for any argument list).

It would be good to allow such a usage mode without introducing the
ambiguity risk and without unnecessary complicating the compilation
process. If such a definition is difficult to find, I can suggest
removing XMR from this proposal, because there are also other ways how
multiple arguments may be handled. My philosophy is (that I am often
blamed for:)) that it is better to impose too restrictive limitations in
the LRM with the ability to drop some of them later, than to allow a too
loose definition which will have to be restricted in the future, thus
introducing a backward incompatibility.

---

On to a few direct notes on your response:

  1) The view the "let" expansion is strictly after elaboration
     is clearly not accurate, or if it is then the current text
     is very deficient.  If one has:
         let x = 10;
         for (genvar i = 0; i < x; i ++) ....
     how can one claim that the "let" is after elaboration?

[Korchemny, Dmitry] I would say that let value should be known before
usage, i.e., if its value is used for elaboration purposes, then it
should be evaluated at the elaboration time. Again, if to disallow let
XMR, then it could be stated that let is evaluated during the
elaboration.

BTW, your example suggests that let is a generalization of genvar, and
maybe these two constructs may be united. What do you think?

---

     Even in the context of types and type parameters this
     can occur (at least it isn't currently restricted):
         let x = 5;
         type(x) y;
         M #(type(x)) m();

[Korchemny, Dmitry] I don't see any issue here. It is equivalent to

type(5) y;
M #(type(5)) m();

---
     or even
         class C (type T = int); ....
         let x(y,z) = C#(y)'(z)

[Korchemny, Dmitry] Same idea here.
---

     All of these have non-trivial elaboration impact and
     seem to be legal in the current proposal.

     Along the same lines, if "let" is post-elaboration, why
     is there any restriction about "existence prior to reference"?
     What does that mean in terms of elab interaction?

     Is the following legal:
         for (genvar i = 0; i < 5; i++) begin : b
            if (i < 4) begin:c
               let x = b[i+1].c.x
            end else begin:c
               let x = 0;
            end
         end
     Does iteration i+1 "exist" at the time iteration i has its
     "let" defined?

[Korchemny, Dmitry] My guess is that this should be illegal. If we
disallow "let" XMR, the issue becomes irrelevant. If we want to allow at
least the use cases as in the above motivation example, there is a need
to provide formal semantics of "generate" statements - then we can
formally define what "existence prior to reference" exactly means.

---

  2) The assertions stuff is not in fact defined in terms
     of "inlining".  It talks about the what the equivalent
     expressions are.  A proposal like this should not
     introduce new terminology.

[Korchemny, Dmitry] OK.
---

  3) No one has as yet addressed the other concerns and
     questions that I raised in my original response.

[Korchemny, Dmitry] Please, see my comments below. If we disallow XMR,
most of the concerns become irrelevant.
---

  4) An additional thought -- one of the key uses for "bind"
     is to allow assertion instances to bind into otherwise
     "pure" rtl.  How does one "bind" an instance which includes
     a "let" expression into a target?  Clearly (I hope!) one can't
     do the syntactic form of expansion that is being suggested.
     Is that illegal?  Is it just something that no tool will
     be able to implement?

[Korchemny, Dmitry] Could you provide a specific example? It is legal to
bind instance with sequences and properties.

---

Gord.





Mark Hartoog wrote:
> Sequences and properties have the same problem with inlining. 
> They are inlined after elaboration.
> 
> The one new problem here is that let can be used in constant
> expressions required for elaboration. Clearly hierarchical references
> to let expressions can not be permitted in constant expressions.
>  
> 
>> -----Original Message-----
>> From: owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] On 
>> Behalf Of Gordon Vreugdenhil
>> Sent: Wednesday, June 06, 2007 3:16 PM
>> To: sv-ac@eda.org
>> Cc: sv-bc@eda.org; sv-ec@eda.org
>> Subject: [sv-bc] Re: [sv-ec] Updated proposal for 'let' syntax
>>
>>
>> Points 5, 6, and 7 appear contradictory.
>>
>>    5)  ... In the scope of declaration, let must be defined 
>> before used.
>>    6) The let expression is inlined ....
>>    7) The let expression can be referenced by hierarchical name...
>>
>> Given:
>>     module top;
>>        int x = some_non_existent_module.some_let_name;
>>     endmodule
>>
>> How does one inline the let expression in the presence of 
>> separate compilation?  Clearly one cannot.
>>
[Korchemny, Dmitry] This is not different from the case of sequences and
properties.

---
>> Any statement of "inlining" is incomplete and not possible in 
>> a general Verilog design.  Any requirements for inlining in 
>> the presence of hierarchical names are in conflict with the 
>> rest of the LRM semantics and must be struck or be 
>> well-defined in terms of the **elaboration** model.
>>
>> (5) also directly conflicts with (7).  If (7) is true, then 
>> the following is legal:
>>     module top;
>>        int x = top.y;
>>        let y = 0;
>>     endmodule
>> But (5) just claimed that you cannot refer to the let before using
it.
>>
[Korchemny, Dmitry] Again, the same situation happens with sequences and
properties

--- 
>>
>>
>> The typing of "let" in hierarchical contexts is not defined.
>> For example,
>>     module M;
>>        let f(x,y) = { x, y };
>>     endmodule
>>
>>     module top;
>>        int q[$];
>>        bit a, b;
>>        bit[1:0] c;
>>        initial begin q.push_back(1); q = M.f(q, 1); end
>>        initial begin c = M.f(a, b); end
>>     endmodule
>>
>>
>> Is "M.f" really supposed to represent queue push in one call 
>> context and bit concatenation in the other?
>> Do people really want to have this be a requirement in the 
>> face of separate compilation?
>>
>>
[Korchemny, Dmitry] This issue is not specific to XMR, you could put the
let definition into the same module. If the syntax is overloaded, it is
what we will get. Consider a more likely example:

module top;
	let f(x,y) = x + y;
	bit [5:0] a, b;
	bit [6:0] c, d;
	... f(a,b)...
	... f(c,d)...
endmodule

Here also the f(a,b) and f(c,d) represent different opeartors, therefore
the question is whether the operator syntax is overloaded on purpose or
not. One could limit the "let" definition to allow only expressions of
integral type - this would filter out such cases of "wild" overloading.
On the other hand this limitation may be unnecessarily restrictive.

>> The proposal doesn't give the grammar changes for where a 
>> let_declaration is legal.  Is it legal in a class?
>> If so then under what circumstances is a "let" static?
>> Given an intentionally incomplete definition:
>>     class C;
>> ...
>>       let something = something_else;
>> ...
>>     endclass
>>     C c = new;
>>
>> Under what conditions is "C::something" valid?  What about 
>> "c.something"?
>>
>>
[Korchemny, Dmitry] You are right, this definition is missing. I think
that let should be part of package_or_generate_item_declaration.
Therefore the above example should be illegal.

>>
>> Given:
>>       let f(x,y) = x + y;
>> Is it (supposed to be) true in all circumstances (including 
>> all context-determined circumstances) that 
>> "<some_hierarchical_path>.f(a,b)" can substitute for "a + b" 
>> without any change in the results of the overall expression?
>>
[Korchemny, Dmitry] I cannot directly think of anything wrong here, but
I agree, we should be careful, and it is better to limit the generality
of this proposal (see my comment in the beginning of this mail).

>> I simply do not buy the suggestion that has been made that 
>> "let" can both act like a function and act like a macro.  I 
>> don't have any problem with having let be a "macro" like 
>> construct in packages where you are guaranteed to have 
>> visibility to the let body PRIOR to use.  That was, I 
>> thought, what the key requirements were.  Unfortunately, this 
>> has become seriously entangled in other constructs where the 
>> interactions are not nearly that simple.
>>
>> The performance implications of implementing this (not to 
>> mention the semantics) for general cases makes me quite 
>> opposed to the generality of this proposal.
>>
>> Gord.
>> --
>> --------------------------------------------------------------------
>> Gordon Vreugdenhil                                503-685-0808
>> Model Technology (Mentor Graphics)                gordonv@model.com
>>
>>
>> -- 
>> This message has been scanned for viruses and
>> dangerous content by MailScanner, and is
>> believed to be clean.
>>
>>
> 

-- 
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com


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