[sv-ac] Re: Mantis 1995 - concurrent assertions in loops

Dmitry,


I think that the 3rd alternative would be the best as far as
I am concerned.  I'll let others consider the semantics with
respect to the checkers; I don't have all of that in my head yet.
The third alternative does not pose any issues that I can
immediately see with respect to any assumptions about a
"semi-synthesized" design (loop unrolling or similar) and deals
with the semantics of the assertions without resorting to
that kind of description.  That, to me, is much more acceptable.

A few direct responses on other points follow.

Korchemny, Dmitry wrote:
[...]
> 
> (1)
> 
>      "A preceding statement shall not invoke a task call that contains a 
>       timing control on any statement."
[...]

> [Korchemny, Dmitry] This limitation does not introduce anything new for 
> assertions in loops, it already exists in LRM for enable condition 
> inference:
> 
>  
> 
> "The enabling condition is inferred from procedural code inside an 
> always or initial procedure,
> 
> with the following restrictions:
> 
> a) There must not be a preceding statement with a timing control.
> 
> b) A preceding statement shall not invoke a task call that contains a 
> timing control on any statement.
> 
> ..."
> 



Well, had I been aware of that back in the 2005 time frame, I would
have vehemently objected to that language as well.


When you want to have separate compilation and hierarchical
referencing of tasks, such a requirement ends up being
very difficult, even more so now with classes and virtual
tasks, etc.  What do you do with a virtual task where only
*some* of the overrides contain delays?  Introduce a run-time
check?  No one wants that.

I think that once again this is a case of the "synthesis" or
local-analysis assumptions creeping in.  But fully general support
can't make those assumptions.

So, please, let's not make the problem worse.  It is already
going to take a potentially incompatible change to fix the
statement you quote -- I don't want to have to deal with that
in two places.


> [Korchemny, Dmitry] There are other kinds of constants required in 
> assertions. E.g., in the assertion  
> 
> assert property(@clk a ##n b);
> 
> n shall be a constant. Why does mentioning constants in this case 
> introduce a new issue?


If you start talking about naming and rewrites it does since the
"name" is now composed of a *value* that we can't possibly know
until elaboration time.  This is part of the 2001 problems that
I referred to earlier.  If we change to the approach (3) that
you raised, this concern goes away.


> [Korchemny, Dmitry] I would prefer to postpone the discussion about 
> foreach loops until the plain for loops with integer indices are 
> understood.

Fine.  But the proposal should not be considered ready until either
things are clarified or "foreach" is removed.


> Is it now the case that one could now hierarchically
> reference through a *sequential* block and find a generate block?
> 
> What is the relationship in terms of authoritative hierarchical
> names between the sequential block structure and the inferred generate?
> 
> How does the pli reach these new generate blocks?  Are they
> really in the same scope?  If so, how does the pli safely
> deal with the different lifetime/scheduling assumptions?
> 
> [Korchemny, Dmitry] One possibility is to allow PLI seeing only one 
> original assertion.


I don't think that will work.  The assertions will certainly include
the constant values from the "generate" unrolling and need to
be distinguished.  Someone the correlation needs to be made.

In the sequential case, you can't inspect the values unless the loop
is active but that is inherently a *sequential* activity and consideration.
If you unroll the loop (or generate it) then the assertions can
be considered at non-sequential points and need to be dealt with
in an independent manner.

> [Korchemny, Dmitry] I would make illegal referencing automatic variables 
> in concurrent assertions, at least in loops.

Be careful here.

The LRM clearly says that for:
    for (int i = 1; ...)
the following applies:
    The local variable declared within a for loop is equivalent to
    declaring an automatic variable in an unnamed block.

So you would disallow any concurrent assertions in such loops.

I'm Ok with that (any restrictions here are fine with me :-)
but I doubt that either you or the general user community will
be.

I think that you'll have to address the automatics in some manner
or the whole use model will be fairly crippled no matter what.



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.