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

Hi Erik,

excuse me but I didn't follow the discussion closely on 1995, but I have
read the proposal now and I have some questions that might have been
answered already in the previous discussion.

First I'm wondering about the intended semantics of the construct.  What
values of the different variables should be used when the (different
instances of the) property are evaluated? Is it the sampled value after
the execution of the entire for loop or is it an itermediate value
arising at the point when the particular istance is "generated"?


For example consider the example in the Objectives section in the
proposal


always @(posedge clk) 
for (i=0; i<MAXI; i=i+1) begin 
    for (j=0; j<i; j=j+1) begin 
       ... table[i][j] <= myfunction(i,j,other_variable); 
       assert property ( table[i][j] != some_expression); ... 
    end 
end

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?

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.


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?

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.

I also have a couple of questions regarding enabling conditions and for loops.

First the rewrite of the example into

always @(posedge clk) begin 
   for (i=0; i<3; i=i+1) begin 
      for (j=0; j<=i; j=j+1) begin : 
         table[i][j] <= myfunction(i,j,other_variable); 
         a1: assert property (foo |-> (bar |-> table[i][j] != `BAD_VAL))); 
                else report_failure(i,j); 
      end 
   end 
end end end

seems incorrect. I think the if clauses need to be retained for the
non-assertion code to be correct: In the rewrite the table gets assigned
even when foo or bar are false.

Second consider the following example:

always @(posedge clk) 
foo = 1'b0;
for (i=0; i<10; i=i+1) begin 
    if (foo) begin
       table[i] <= myfunction(i,other_variable); 
       assert property ( table[i] != some_expression);
    end
    foo = !foo;
end

I don't know whether this is the correct way to code it but my intention
is that foo is a variable that gets toggled at each iteration of the
loop hence only every other position in table gets assigned.

Now the proposal seems to imply that 10 (for 0<=m<10) instances of the
property should be generated:

       assert property ( foo |-> table[m] != some_expression);

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

       assert property ( 1'b0 |-> table[0] != some_expression);
       assert property ( 1'b1 |-> table[1] != some_expression);
       assert property ( 1'b0 |-> table[2] != some_expression);
                            ...
       assert property ( 1'b1 |-> table[9] != some_expression);

or is it the sampled value in which case we seem to get

       assert property ( 1'b1 |-> table[0] != some_expression);
       assert property ( 1'b1 |-> table[1] != some_expression);
       assert property ( 1'b1 |-> table[2] != some_expression);
                            ...

Best Regards,

Johan M


On Mon, Nov 19, 2007 at 12:46:22PM -0800, Seligman, Erik wrote:
> PDF also included here for reference.  This version addresses the main
> issues that Gord brought up, replacing the generate-based rewrite with a
> more procedural description.
>  
> Those of you who had an interest in this one-- pls take a look and tell
> me if your concerns are addressed.  
>  
> Thanks!
>  
>  
> Erik Seligman
> 
> Formal Verification Architect
> 
> Corporate Design Solutions
> Design Technology and Solutions
> 
> M.S. JF4-402                   
> 2111 NE 25th Ave
> Hillsboro, OR 97124 
> 
> Phone:   (503) 712-3134
> 
>  
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 



-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

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