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.