RE: [sv-ac] Review of Mantis 1995 Proposal

From: Bustan, Doron <doron.bustan_at_.....>
Date: Sun Sep 23 2007 - 23:40:45 PDT
I am not very familiar with SV history, but as far as I remember,
the only reason that global variables can be used as 'for loop' control
variables, is backward compatibility. There are no advantages and at
least one disadvantage.
There are no backwards compatibility issues with 1995, so why give users
a rope to hang themselves? Does anybody aware of an advantage of using
global variables as 'for loop' control variables?

Doron


-----Original Message-----
From: Korchemny, Dmitry 
Sent: Sunday, September 23, 2007 5:13 PM
To: Bustan, Doron; Bresticker, Shalom; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] Review of Mantis 1995 Proposal

Hi Doron,

I agree with Shalom and I think that a note would be sufficient here,
that the rewriting rule does not check whether the loop variables change
externally. Such code is very rare and the users shall not put
concurrent assertions there. EDA tools may issue a warning in this case.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Bustan, Doron
Sent: Sunday, September 23, 2007 1:56 PM
To: Bresticker, Shalom; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] Review of Mantis 1995 Proposal

I don't have access to the original code but something like that may
expose the problem.


module foo(input clk, input [0:1] c);
  int i;
  logic [0:1] a,b;

  always @(*) for (i = 0 ; i < 1 ; i++) a=c;
  always @(*) for (i = 0 ; i < 1 ; i++) b=c;

  a1: assert property(@(posedge clk) b == a);

endmodule

It is consistent with 12.7.1 :

"The variables used to control a for-loop can be declared prior to the
loop. If loops in two or more parallel processes use the same loop
control variable, there is a potential of one loop modifying the
variable while
other loops are still using it.

The variables used to control a for-loop can also be declared within the
loop, as part of the for_initialization assignments. This creates a
local variable within the loop. Other parallel loops cannot
inadvertently affect
the loop control variable."

Doron

-----Original Message-----
From: Bresticker, Shalom 
Sent: Sunday, September 23, 2007 1:14 PM
To: Bustan, Doron; 'sv-ac@server.eda-stds.org'
Subject: RE: [sv-ac] Review of Mantis 1995 Proposal

Can you send the exact example?

Shalom 

> -----Original Message-----
> From: Bustan, Doron 
> Sent: Sunday, September 23, 2007 1:11 PM
> To: Bresticker, Shalom; Seligman, Erik; 
> 'Thomas.Thatcher@sun.com'; 'sv-ac@server.eda-stds.org'
> Subject: RE: [sv-ac] Review of Mantis 1995 Proposal
> 
> I saw the problem in a simulator of a known vendor.
> As far as I understand it, the simulator did not do anything illegal.
> 
> Doron
> 
> -----Original Message-----
> From: Bresticker, Shalom
> Sent: Sunday, September 23, 2007 1:09 PM
> To: Bustan, Doron; Seligman, Erik; 'Thomas.Thatcher@sun.com'; 
> 'sv-ac@server.eda-stds.org'
> Subject: RE: [sv-ac] Review of Mantis 1995 Proposal
> 
> The problem is theoretical.
> 
> In practice, if the loop does not contain any time-consuming 
> statements, the problem does not occur.
> 
> One could instead write a caveat emptor sentence.
> 
> Shalom 
> 
> > -----Original Message-----
> > From: Bustan, Doron
> > Sent: Sunday, September 23, 2007 12:56 PM
> > To: Bresticker, Shalom; Seligman, Erik; 'Thomas.Thatcher@sun.com'; 
> > 'sv-ac@server.eda-stds.org'
> > Subject: RE: [sv-ac] Review of Mantis 1995 Proposal
> > 
> > Because the assignments to i are parallel, it could be that 
> i will be 
> > increased in the second block before it will be referenced in the 
> > first block.
> > 
> > This is a general problem in verilog and the simple solution is to 
> > write
> > 
> > for (int i = 0 ; i < 3 ; i++)
> >     assert property (a(i));
> > 
> > 
> > for (int i = 0 ; i < 3 ; i++)
> >     assert property (b(i));
> > 
> > Doron
> > 
> > 
> > -----Original Message-----
> > From: Bresticker, Shalom
> > Sent: Sunday, September 23, 2007 12:51 PM
> > To: Bustan, Doron; Seligman, Erik; Thomas.Thatcher@sun.com; 
> > sv-ac@server.eda-stds.org
> > Subject: RE: [sv-ac] Review of Mantis 1995 Proposal
> > 
> > Why not?
> > 
> > Shalom
> > 
> > > -----Original Message-----
> > > From: owner-sv-ac@server.eda.org
> > > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Bustan, Doron
> > > Sent: Sunday, September 23, 2007 9:14 AM
> > > To: Seligman, Erik; Thomas.Thatcher@sun.com;
> > sv-ac@server.eda-stds.org
> > > Subject: RE: [sv-ac] Review of Mantis 1995 Proposal
> > > 
> > > If you allow any variable as the control variable, then you
> > may not be
> > > able to extract a compile time range/ for example if you have 
> > > something like
> > > 
> > > int i ;
> > > 
> > > for (i = 0 ; i < 3 ; i++)
> > >     assert property (a(i));
> > > 
> > > 
> > > for (i = 0 ; i < 3 ; i++)
> > >     assert property (b(i));
> > > 
> > > then you are not guaranteed to have a(0), in the code.
> > > 
> > > Doron
> > > 
> > > -----Original Message-----
> > > From: Seligman, Erik
> > > Sent: Thursday, September 20, 2007 7:26 PM
> > > To: Bustan, Doron; Thomas.Thatcher@sun.com;
> > sv-ac@server.eda-stds.org
> > > Subject: RE: [sv-ac] Review of Mantis 1995 Proposal
> > > 
> > > Hi Doron-- what is the motivation for this restriction?   
> > > 
> > > -----Original Message-----
> > > From: owner-sv-ac@server.eda.org
> > > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Bustan, Doron
> > > Sent: Sunday, September 16, 2007 4:24 AM
> > > To: Thomas.Thatcher@sun.com; sv-ac@server.eda-stds.org
> > > Subject: RE: [sv-ac] Review of Mantis 1995 Proposal
> > > 
> > > I also think that it in a good condition. One comment:
> > > 
> > > I would add to the items list on 16.14.5:
> > > 
> > > "The variables used to control a for-loop shall be declared
> > within the
> > > loop, as part of the for_initialization assignments."
> > > 
> > > Doron
> > > 
> > > 
> > > -----Original Message-----
> > > From: owner-sv-ac@server.eda.org
> > > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Thomas Thatcher
> > > Sent: Saturday, September 15, 2007 3:25 AM
> > > To: sv-ac@server.eda-stds.org
> > > Subject: [sv-ac] Review of Mantis 1995 Proposal
> > > 
> > > Hello Everyone,
> > > 
> > > I have reviewed Mantis 1995.  It looks fairly straightforward.  I 
> > > didn't find anything wrong with it.
> > > 
> > > Tom
> > > --
> > > ------------------
> > > Thomas J. Thatcher
> > > Sun Microsystems
> > > 408-616-5589
> > > ------------------
> > > 
> > > --
> > > 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.
> > > 
> > 
> ---------------------------------------------------------------------
> > > 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.
> > > 
> > 
> 
---------------------------------------------------------------------
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.
---------------------------------------------------------------------
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.
Received on Sun Sep 23 23:41:14 2007

This archive was generated by hypermail 2.1.8 : Sun Sep 23 2007 - 23:41:32 PDT