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

I finally found some time to take a look at this.

A few comments below (See "GORD:")


Seligman, Erik wrote:
> Hi guys--  I'm starting to rewrite this proposal.  Based on the 
> discussions, it sounds like the major issue is the concept of rewriting 
> an assertion as a generated loop of assertions, so we need to create a 
> way to describe these things as covering all loop elements while still 
> leaving them as a single assertion for reference & compilation 
> purposes.  Below I have a short outline of two approaches; can those of 
> you who are interested send comments on which approach you prefer, and 
> whether you think one or both is fatally flawed?  Thanks!
>  
> BTW:  we should note again that the concurrent-asserts-in-loops feature 
> is already something we use in our designs, and drive our vendors to 
> implement.  So if we fail to standardize this, it's not that vendors 
> won't end up having to implement the feature-- it's just that it will be 
> implemented in haphazard ways that are different for each vendor.  Thus 
> I really think getting this proposal to work in some form is something 
> that should be done for this standard.
>  
>  
> 1.  (Dmitry's option #3, trying to rephrase without a dependency on free 
> variables in 1900).   The assertion in the loop is treated as a non-loop 
> assertion except that the loop iterators can be freely assigned to any 
> set of values in the defined ranges.   So for each possible set of 
> values, the assertion is executed with those values, and the action 
> block is then executed if applicable for those same values.  So, as in 
> Dmitry's email, look at:
> 
> b1: for (int i = 1; i < 3; i++)
> 
>       b2: for (int j = 0; j < i; j++)
> 
>             // p is some property dependent on i and j
> 
>             a: assert property(@clk p(i,j)) pass_action(... i, j, ...); 
> else fail_action(... i, j, ...);
> 
>  
> 
> In order to check assertion a, property p(i,j) is checked respectively 
> for (1,0), (2,0), and (2,1), with pass_action and fail_action possibly 
> being executed for each set of values.   But for hierarchical reference 
> purposes, this is still one assertion, 'a'.
> 
>  
> 
> Comments:
> 
>     - Nice overall solution that preserves full functionality.
> 
>     - Question about whether this separate property checking for each 
> set of values, while still remaining a single property, will 
> be acceptable to simulator-oriented reviewers (Gord?).


GORD:

I think that this is a very reasonable way in which to talk
about things.  It separates the real issue -- evaluation over
some universe of inputs -- from the details of *how* an
implementation chooses to do the evaluation.  It would be
equally valid to "unroll" the loop (as a semi-synthesized
approach might do) or to "box up" the loop bounds.  The
implementation is responsible for retaining the conceptual
structure of the design.

I am assuming that the same "enable" restrictions apply, yes?

So, if you have:
        if (i > 1)
            a: assert ...
that the "enable" will involve the value of "i" and "j".

I think that this is still Ok since other non-loop variables
must be static.  The loop vars conceptually still just
range over all the bounds and the enable is described
in terms of that.



The main difference here, is that you are *defining*
a structural rewrite.  You are simply defining the
assertion's evaluation behavior.  That has a much
better kind of interaction with the rest of the LRM --
you don't bring naming issues, structure, etc. into
play at all.

Depending on how this is worded, this could even open
up what I think is a desirable independence of the
assertions (likely what you are assuming) -- that it
doesn't matter in which order the loop values are applied,
they just all have to be considered.

I think that due to the comfort that various people
have with "synthesis" approaches, there is a real bias
towards trying to define a synthesis-like structural
rewrite.  Avoiding that and just talking about the abstract
*behavior* bypasses the issues that I have been raising.
The above approach does that very nicely and will likely
lead to a more concise description in any case.


> 2. (Conservative definition, very simple preservation of single-property 
> concept):  The assertion in the loop is treated as a single assertion on 
> the AND of the conditions for each iteration.   The action blocks are 
> expanded into conditionals that execute on temporary variables depending 
> on which values fail the assertion.  For example: 
> 
>  
> 
> b1: for (int i = 1; i < 3; i++)
> 
>       b2: for (int j = 0; j < i; j++)
> 
>             // p is some property dependent on i and j
> 
>             a: assert property(@clk p(i,j)) pass_action(... i, j, ...); 
> else fail_action(... i, j, ...);
> 
>  
> 
> b2.a is equivalent to
> 
>                             assert property (@clk ((p(1,0) and p(2,0) 
> and p(2,1)))  
> 
>                                 { pass_action{....1,0...}; 
> pass_action{...2,0...}; pass_action{...2,1...}} else
> 
>                                 { p(1,0) ? pass_action(.... 1, 0...) : 
> fail_action{.... 1, 0...);
> 
>                                  p(2,0) ? pass_action(.... 2, 0...) : 
> fail_action{.... 2, 0...);
> 
>                                  p(2,1) ? pass_action(.... 2, 1...) : 
> fail_action{.... 2, 1...);}
> 
>  
> 
> Comments:
> 
>     - Less elegant than above, but creates explicit single assertion, so 
> may be more acceptable?



GORD:

I'd have to think about the enable conditions in such an
expansion.  I think it would work, but I think the first
option is much more clean.


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.