RE: [sv-ac] #1502 (Property evaluation attempts and decision points)

Hi all,

I uploaded a new version. Your review will be appreciated.

Thanks,
Dmitry

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Friday, June 16, 2006 6:06 PM
To: Korchemny, Dmitry
Cc: sv-ac@verilog.org
Subject: Re: [sv-ac] #1502 (Property evaluation attempts and decision
points)

Hi Dmitry:

I know you said that you are revising your proposal, but I 
am confused about your motivating example.

\top satisfies both a and !a, so taking j <= 1000, I think

  w^{0,j-1}\top^\omega |=  1 |-> ((##1000 a) and (##1000 !a)) 

Thus, it seems that for the property "1 |-> ((##1000 a) and (##1000
!a))",
B is the set {1001,1002,...} and the failure point is 1001.

[BTW, I think I would avoid shifting these points from the word
indexes to keep things simpler, i.e. use "w^{0,j}" instead of 
"w^{0,j-1}" in the definitions of A and B.]

Best regards,

John H.


> X-Authentication-Warning: server.eda-stds.org: majordom set sender to
owner-sv-ac@eda-stds.org using -f
> X-IronPort-AV: i="4.06,137,1149490800"; 
>    d="scan'208,217"; a="51353822:sNHT4453369242"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 15 Jun 2006 18:59:22 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: #1502 (Property evaluation attempts and decision points)
> thread-index: AcaQlKsZItCfAO9SQOOChKem5WC7fw==
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 15 Jun 2006 15:59:45.0740 (UTC)
FILETIME=[B8D898C0:01C69094]
> X-Virus-Status: Clean
> Sender: owner-sv-ac@eda-stds.org
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C69094.AB5B43BA
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: 7bit
> X-Former-Content-Transfer-Encoding: quoted-printable
> 
> Hi all,
> 
>  
> 
> Following our last meeting minutes I am submitting a Mantis item
> containing a formal definition of an assertion attempt failure and
> success (=decision) points. I am giving an inductive definition which
is
> rather sophisticated. A simple definition as 
> 
>  
> 
> Let $A = \{j| w^{0,j-1}\bot^\omega \models P\}$. $i$ is a property
> success point iff $A \ne \emptyset$ and $i = \min{A}$.
> 
> Let $B = \{j| w^{0,j-1}\top^\omega \nvDash P\}$. $i$ is a property
> failure point iff $B \ne \emptyset$ and $i = \min{B}$.
> 
>  
> 
> does not  look good, since in such a case we would have to report the
> failure of the following property
> 
>  
> 
> 1 |-> ((##1000 a) and (##1000 !a)) 
> 
>  
> 
> at the initial cycle. Most tools won't detect the failure before the
> 1000th cycle, however.
> 
>  
> 
> Any formal definition of a decision point has the drawback that it
> forbids any optimizations during simulation. On the other hand, it
looks
> strange if there is no exact definition of the time when the action
> block should be executed. I am also concerned about integrating an
> automata-oriented simulation approach with this definition.
> 
>  
> 
> Thanks,
> 
> Dmitry
> 
>