RE: [sv-ac] dynamic variables for expect

Hi Manisha,

 

Sorry for miss understanding.

 

I am not very familiar with automatic variables (nor SV threads in
general),

So I wouldn't volunteer for that task... 

 

I don't understand what happen to an assertion on automatic variables
for which during its evaluation there is a fork.

Does the assertion attempt splits? Is there a well defined "thread based
view" of all variable (automatic and static)

For which we can define sample value?

 

I guess that similar questions should be asked about expect, I am not
sure what to say.

 

Doron

 

________________________________

From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com] 
Sent: Friday, September 21, 2007 7:43 AM
To: Bustan, Doron; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] dynamic variables for expect

 

Hi Doron,

 

I am not able to find the meeting minutes for the meeting where we
discussed this issue. As far as I remember the issues was about allowing
automatic variables (not dynamic variables). Currently 1549 puts this
restriction that only static variables can be passed as arguments to
properties and sequences. Since expect allows usage of automatic
variables, I raised the question if we should put this restriction or
not.

 

Thanks.

Manisha

 

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Bustan, Doron
Sent: Sunday, September 02, 2007 5:21 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] dynamic variables for expect

 

In the last meeting I took an assignment to check the implications of
referencing dynamic 

variables in expect on properties.

 

My main concern was that it will make the model checking of SVA
un-decidable. I think that

we should try to avoid that.

 

My conclusions are:

 

1.	Once the design includes dynamic variables, SVA become
un-decidable even

       without direct references to the dynamic variables. I did not
proved it, but my intuition 

       is that every Turing machine can be represented by pure Verilog +
two queues. In this 

       case the (fix size) transition relation can be represented by
verilog logic, the tape left to 

       the head of the Turing machine by one queue and the tape to the
right of the head by the 

       other queue. In this case a Boolean property referencing a
verilog variable may determine 

       whether the Turing machine halt, and this is un decidable.

 

2.	 As far as I can tell if there are no syntactic restrictions
that limit the dynamic variables length 

Or the length of the property evaluation to a compile-time bound, then
deciding whether model 

checking of a specific design is decidable, is by itself un-decidable.
(This is a practical statement, 

             I am sure that one can come with non-practical restriction
that do not bound the size but live the problem decidable.)

 

3.	As far as I can tell, if there are syntactic restrictions that
limit the dynamic variables length to a compile-time bound, then

referencing them, or even using them as actual arguments will not  make
the model checking of the properties un-decidable.

 

 

Bottom line : 

*         Do not try to use formal tools on designs with dynamic types.
Be very careful in simulation.

*         Referencing dynamic types or using them as actual arguments,
will not make a situation worth.

*         I don't think that we need to change the language of 16.16.

 

Doron

 


-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , 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.