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

Hi Gord,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: Gordon Vreugdenhil [mailto:gordonv@model.com] 
Sent: Monday, June 11, 2007 5:20 PM
To: Korchemny, Dmitry
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


I've tried to narrow this down to just the portions with my
responses.

Korchemny, Dmitry wrote:
[...]

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


I'd be willing to step out of this entire discussion if a
"let" was only permitted to be evaluated in the context of
another "let" or in the context of a sequence or property.
Then it really is the same thing and any tool issues are isolated
from the rest of the language.

It is the fact that "let" is *not* restricted in its domain of
application that makes me concerned.

[Korchemny, Dmitry] Though let by its nature is applicable to different
areas of the language, and not to properties only, upon a discussion in
SV-AC we decided to modify our proposal to limit let usage to
properties. Nevertheless, we are going to define it in a way allowing
later extension if needed and wanted.

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


I really do not understand this as a compelling example.
Why is this any different than "args.sum()" ?  Or a function
that sums "args"?  Or a function in each gen block that
hierarchically calls the other?

What is special about what you are doing here that requires
"let"?

[Korchemny, Dmitry] The idea is to find a mechanism to define sequences
and properties with a variable number of arguments, and "let" can
provide a potential solution. Same idea is applicable with corresponding
modifications to functions, tasks, modules, etc. Let's consider an
example of a property checking that its arguments have the same value.
At present I have to write different implementation for different number
of arguments:

property same2(a1, a2);
	a1 == a2;
endproperty

property same2(a1, a2, a3);
	a1 == a2 && a1 == a3;
endproperty

...

I want to write something like:

property same(*a);
	for (genvar i = 1; i < $size(a); i++) begin b1
		if (i == 1) begin : b2
			let res = $argv(a, 0) == $argv(a, i);
		end
		else begin : b2
			let res = b1[i-1].res && $argv(a, 0) == $argv(a,
i);
		end
		res;
endproperty

I am using constructs here that are not part of the language: syntax for
variable number of arguments (*a means that a is a list of arguments,
etc), using generate and let statements within a property statement, but
this example illustrates the idea.

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


XMR's are already disallowed here -- Rule 14 requires that since
"x" is constant expression, it is legal only if the equivalent
constant function is legal (i.e. no xmr to "x" and no xmr's
within "x").

That wasn't the point of this in any case -- the point was that
"x" **MUST** participate in elaboration since it is one of
the generate loops bounds.  Mark's contention was that "let"
occurs after elaboration.  If this example is legal, clearly
that contention is not correct.  If this example is not legal
then the proposed rules are deficient in that this is permitted
by the rules.

[Korchemny, Dmitry] Whenever "let" results are used during elaboration,
"let" should be processed during the elaboration. The leftovers need to
be processed after it. This case is not unique in SV: e.g., constant
functions are evaluated at or before the elaboration time, while other
functions are evaluated at the simulation time.

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


No -- "x" in this construct is not a genvar at all -- it is a
constant expression that happens to be a "let" evaluation.

It depends on the exact definition. One can slightly modify the
definition to make these constructs very similar. It is enough to say
that let may be redefined in the same scope to get the desired effect:

let x = 1; // = 1
let x = x + 2; // = 3

genvar keyword may even be reused:

genvar x = 1; // = 1
genvar x = x + 2; // = 3

Then the above example can be rewritten in a more elegant way as:

property same(*a);
	genvar res = 1'b1;
	for (genvar i = 1; i < $size(a); i++) begin b1
		genvar res = res && $argv(a, 0) == $argv(a, i);
	end
	res;
endproperty

To be clear I am not suggesting necessarily defining it this way, but
just pointing out to the similarity between both constructs.

> ---
> 
>      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();


Again, it just means that "let" participates in elaboration in all
sorts of interesting ways.  You *cannot* insulate "let" from elaboration
if you claim that these are legal.

[Korchemny, Dmitry] See my comment above

> 
> ---
>      or even
>          class C (type T = int); ....
>          let x(y,z) = C#(y)'(z)
> 
> [Korchemny, Dmitry] Same idea here.


Really?  Note that "y" here must be a *type*.

I don't really think this would be legal in any case since the grammar
restricts a let actual to being an expression.

[Korchemny, Dmitry] Agree

But one could have a partially mixed expression --
    typedef int y;
    let x(z) = C#(y)'(z);

Now you don't know whether C#(int) exists until you know whether the
"let" is actually used.

[Korchemny, Dmitry] Correct

  This also causes a specialization that
is a mix of local and remote references.  If this is within a class
and "y" is a local typedef, there isn't even a legal corresponding
source expression.

[Korchemny, Dmitry] I am not sure I understand your concern.

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

I agree, without XMRs this is trivially illegal.  That is why I
made that suggestion; it gets rid of many problems.

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

NO!!!!  That is *exactly* my point.  By intent, Verilog talks about
relationships between objects and *results* of elaboration.
Requiring an *operational* model for generates would severely constrain
implementations and would likely make various general flows that
tools support considerably weaker.

[Korchemny, Dmitry] I cannot agree with this statement. Unless you have
a formal definition, you cannot guarantee a consistent behavior of
different tools, and this is what we have in practice, even with
different tools of the same vendor, and this problem is not related to
"let". Formal semantics and the operational model of generate does not
prescribe a specific algorithm for the implementation, but requires that
the results of the implementation algorithm be consistent with the
operational model.

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


It isn't the *body* that is the problem, it is the *actuals*.
    bind top.mid.bot M m(a,b,c);

What is "a" is a "let" that is defined in "top.mid.bot"?  In order
to use the "let" in the macro-like manner that is being proposed,
one would have to defer way too much until "bind" time.  In particular,
if "let" can create new class specializations, you would have to
deal with that interaction at bind time.

Requiring this would break very important tool flows where "bind"
occurs very late -- well after the target (typically the dut) is
compiled.  I really do not think that the user community would
be happy with that.

[Korchemny, Dmitry] I don't think so. a should have already been
substituted at the point of bind, and let is not visible at this point.
In your example we'll just have a compilation error that a is not
defined.

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

(1) - if you want to make implementation assumptions within the
assertions
       sublanguage, I don't care too much.  I do care if those
assumptions
       bleed over into the core language.  I think the assertions
assumptions
       are fundamentally flawed and don't lead to large scale efficient
       design unless there are vendor restrictions.  Such restrictions
are
       not going to be the same for every vendor and will be frustrating
       to users.

[Korchemny, Dmitry] If you think that something goes wrong with the
current definition of assertions you are welcome to fill a mantis and we
will consider it. There is not important where inefficiency comes from,
it should be addressed in any case. From the implementer's point of view
the overhead in this case is minimal: the existing code may be reused
with minor changes. I don't see essential difference between "let"
statements and module parameterization as for compilation efficiency is
concerned. If the tools can efficiently deal with parameterized modules
and classes, they will also be able to deal with the above example as
well.

(2) - My comment was that requiring "inlining" and "declaration before
use"
       is fundamentally at odds with the hierarchical name assumptions
       in Verilog.

[Korchemny, Dmitry] Can you assign a variable in a function before you
declare it?

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


So, why is there any "declaration before use" requirement whatsoever?

If all of these follow full Verilog rules then you should not be
trying to explain the name binding.  If there are special restrictions,
talk about them.

[Korchemny, Dmitry] Indeed, I could not find this restriction for
sequences in the LRM. I think that for the implementer's point of view
defined before use is more natural for non-hierarchical names. We need
to revisit this definition.

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

This is a much simpler example -- the *operations* are still
arithmetic, just the widths are different.  Having the *semantic
meaning* of a token change in a "let" expansion implies a really
nasty implementation model.

[Korchemny, Dmitry] This is a semantic change, even if it manifests in
the length difference only. More than that, the operators may be
explicitly overloaded using bind, therefore the result of '+' may be of
any type.

> On the other hand this limitation may be unnecessarily restrictive.

That depends on your assumptions.

If you are going to *require* a source-level implementation model, then
you are assuming that ALL SOURCE is available at the time of design
elaboration.  I really don't think IP providers, etc. are going to
be very happy about that.  That also wreaks havoc with large scale
separate compilation.

[Korchemny, Dmitry] What happens with parameterized modules and classes?
Also, it is up to the IP providers not to expose their "let" statements
and not to use let XMRs in their designs.

Of course vendors can (and will) restrict such behavior, but do
you really want to be adding things to the language that are
specified in such a way that there will necessarily be vendor
restrictions, etc.?  I do not see that as being a good approach
to language design.

[Korchemny, Dmitry] This was not my intention.

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


Ok, that deals with the "class" example.  By construction then, one
also cannot have a "let" inside a sequential block, right?

[Korchemny, Dmitry] Oops, I would include it to block_item_declaration
as well.

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.