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

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

 

 

 

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?

   

 


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.