In today's meeting I was expressing concerns over the typing of "let".  Here is an overview of the typing issue that I am worried about:

    property p(a);
        a + 2 or a + 8'b10;
    endproperty

    bit signed [3:0] x;
    bit signed [3:0] y;
    let my_let = x + y;

    assert p (my_let);

Under the inlining semantics the property "p" expands to:

        x + y + 2 or x + y + 8'b10;

But the two subexpressions "x + y" have different behavior for x and y.  In the first subexpression the overall type is signed and x and y sign extend to 32 bits before doing the addition.  In the second subexpression x and y extend in an unsigned manner due to the presence of the unsigned term.
As a result, if "x" and "y" are both "-1" the assertion will pass since the second subexpression will have the value "32"
rather than 0.

So in considering "my_let" in "assert p (my_let)" you cannot evaluate "my_let" as an expression "a + b" in the context of the assertion instance.  It isn't just that the type of "a + b" depends on the context inside the assertion, but it is also that there is NO single type that works.  This is a pretty fundamental compositional assumption of the current inlining semantics.

In most cases, what I've seen argued are cases such as:

    property p(a);
        (|a);
    endproperty

Where the only real requirement is that "a" be able to express a value of an unknown width.  That is a much simpler problem in that one could easily consider this as being syntactic sugar for:
    property #(type T) p (T a);
        (|a);
    endproperty
with calls being rewritten as:
    assert p#(type(actual)) (actual).

My key concern is that for the first example NO such rewrite is possible if we must keep the existing inlining assumptions.




Here is a situation that concerns me:

    module top;
       assert a.b(c.d, e.f);
    endmodule


Now compile "top" without ANY other context.  In fact, in Verilog, there is no requirement that any of "a", "c" or "e" even exist until elab.  Composing this requirement with the above assumptions about "let" is very problematic when extrapolated to large designs, separate compilation, and the like.

One could define away the problem in an implementation by requiring "definition before use" (or simultaneous
compile) of references to assertions constructs.  But such requirements are again at odds with the elaboration assumptions about configurable designs, libraries, etc.  These are the areas where I would expect vendor restrictions and assumptions to heavily impact actual use flows and become non-portable.

As a comparison point, packages are different -- the LRM requires definition before use for packages and as such, references into a package are much tighter.  If one would restrict references to "let" constructs to things either within the same design element or to within packages, I wouldn't have any problems with "let".  Since the vast majority of real requirements that I have seen center on package encapsulation of assertions constructs rather than arbitrary hierarchical use, it seems that this would be something that could be considered.

-- ErikSeligman - 09 May 2008