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

Well, I don't think it's a language-correctness issue, in that the
behavior is well defined.
However, I do think it's a user confusion issue-- chances are, in
Johan's examples, the user will see behavior different from what they
intended.

Maybe because of this, the rule I suggest below should be '...tools may
generate a warning...' rather than '...shall not be permitted...'?
Either way, I think I need to add a similar example to the proposal, to
clarify.


-----Original Message-----
From: Korchemny, Dmitry 
Sent: Tuesday, November 27, 2007 7:52 AM
To: Seligman, Erik; johan.martensson@jasper-da.com
Cc: 'sv-ac@eda-stds.org'
Subject: 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.)


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