RE: [sv-ac] New version of 1995 (concurrent assertions in loops) proposal posted

Hi Erik, Johan,

Why should this be an issue? Concurrent assertions use sampled values:
loop variables are the only exception.

Thanks,
Dmitry

-----Original Message-----
From: Seligman, Erik 
Sent: Tuesday, November 27, 2007 5:49 PM
To: Johan M?rtensson
Cc: sv-ac@eda-stds.org; Korchemny, Dmitry
Subject: RE: [sv-ac] New version of 1995 (concurrent assertions in
loops) proposal posted

 
Hi Johan--

You point out some important areas that might confuse users.  I wonder
if we should add a rule prohibiting concurrent assertions in loops from
referencing non-iterator or non-iterator-indexed variables modified
within the loop body, to prevent most of these scenarios.  Would this
work?  


> For this particular example I understand the proposal to say that for
any m and n such that 0<=m<MAXI and 0<=n<m the property 
>       assert property ( table[m][n] != some_expression);
> Should be checked. I.e. different instances of the property should be
genereated for all the intermediate values of the 
> iterators, but for all other variables the sampled values should be
used, right?

Correct.

> So for example if 'table' gets modified "after" the assertion so that
the sampled value of 'table[m][n]' is different from the value of
'table[m][n]' at the point where the property instance gets instantiated
as for example in
> always @(posedge clk)
> for (i=0; i<MAXI; i=i+1) begin 
>        table[i] <= i; 
>        assert property ( table[i] == i);
>       table[i] <= i+1; 
>    end
> end
> then it is the sampled value of 'table[m] == m' that should be used so
the instances of assert will all fail.

Correct.  Since a concurrent assertion was used, sampled values are what
we are checking.


> Now assume that for some reason sobody wrote
> always @(posedge clk)
> for (i=0; i<MAXI; i=i+1) begin 
>    for (j=0; j<i; j=j+1) begin 
>       k = i;
>       h = j;
>       table[i][j] <= myfunction(i,j,other_variable); 
>       assert property ( table[k][h] != some_expression);
>    end
> end
> Should this also result in different property "instances" or only one
stating 'table[k][h] != `BAD_VAL' for the sampled values of table, k and
h?

I believe as the proposal is currently stated, the property  (
table[k][h] != some_expression) must be checked for all values of i and
j, but it does not explicitly prescribe whether a tool is allowed to
identify sets of values that result in an equivalent expression and
optimize to only check once.  So if the property fails for the sampled
values of k and h, we can get one report or multiple identical reports.

Do you think we need to make a more explicit rule here?


> Btw what about
> always @(posedge clk)
> for (i=0; i<MAXI; i=i+1) begin 
>    for (j=0; j<i; j=j+1) begin 
>       k = i;
>       h = j;
>       table[i][j] <= myfunction(i,j,other_variable); 
>       assert property ( table[k][h] == table[i][j]);
>    end
> end
>Should this result in the instances 
>
>       assert property ( table[k][h] == table[0][0]);
>       assert property ( table[k][h] == table[0][1]);
>                       ..=
> or in the instances 
>       assert property ( table[0][0] == table[0][0]);
>       assert property ( table[0][1] == table[0][1]);
                       ...

> I don't think the proposal clearly states for which variables the
sampled value should be used and for which the value at the particlular
iteration that gives rise to the property instance.

Maybe we should make this more clear in the proposal:  since it's a
concurrent assertion, everything is sampled values (as in your first set
of "instances") except the loop iterators.  


> I also have a couple of questions regarding enabling conditions and
for loops.
> First the rewrite of the example into ...

You're right, there's a problem in the example-- the rewrite is only
valid for the assertion, not the table[i][j] assignment.


> Second consider the following example:
> The question is: What value of 'foo' should be used? Is it the value
when the property is instantiated so that we get

I believe it would have to be the sampled value.  So if the condition
depends on the loop iterator, the wrong result may be obtained (again, I
think the rule above would prevent this.)

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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