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

Although the LRM does say such things here and there (e.g., 11.4.14,
23.7), we usually don't, because a tool may issue a warning whenever it
wants to, even if the LRM does not say anything. Rarely the LRM may say
not to give a warning, and even then a tool may have a switch to enable
the warning anyway. 

(I can already imagine a switch to issue warnings at random...)

However, it is legitimate for LRM to note that a certain code may do
something other than what the user expected (i.e., "gotcha"), etc.

Regards,
Shalom 

> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of Seligman, Erik
> Sent: Tuesday, November 27, 2007 5:58 PM
> To: Korchemny, Dmitry; johan.martensson@jasper-da.com
> Cc: sv-ac@server.eda-stds.org
> Subject: 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.
> 
---------------------------------------------------------------------
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.