[sv-ac] RE: Mantis 2904

I am proposing to change Dana's sentence to:

If the disable condition becomes is true at anytime between the start of the observed region of the time step in which the evaluation attempt begins and the end of the evaluation attempt.

Thanks,
Samik

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Prabhakar, Anupam
Sent: Tuesday, September 21, 2010 1:23 PM
To: sv-ac@eda.org
Subject: [sv-ac] FW: Mantis 2904

_____________________________________________
From: Kulshrestha, Manisha
Sent: Tuesday, September 14, 2010 11:16 PM
To: Prabhakar, Anupam; 'john.havlicek@freescale.com'
Cc: 'Eduard.Cerny@synopsys.com'
Subject: RE: Mantis 2904

Hi,

This looks fine to me.

Manisha

_____________________________________________

From: Prabhakar, Anupam

Sent: Thursday, September 09, 2010 10:31 AM

To: Kulshrestha, Manisha; 'john.havlicek@freescale.com'

Cc: 'Eduard.Cerny@synopsys.com'

Subject: RE: Mantis 2904

Hi Manisha,

 I see what you are saying - I guess it is tough to explain this. How about

'If the disable condition is true at the point of starting a new evaluation attempt, that attempt shall not start and the property is considered to have a disabled evaluation for this time.'

Or can you think of a better way to explain this.

Anupam

_____________________________________________
From: Kulshrestha, Manisha
Sent: Wednesday, September 08, 2010 9:40 PM
To: Prabhakar, Anupam; 'john.havlicek@freescale.com'
Cc: 'Eduard.Cerny@synopsys.com'
Subject: RE: Mantis 2904

Hi Anupam,

But this change will require that even in the case where .triggered is at a different clock, the property has disabled evaluation as you are considering the whole Observed region. So, in the case of boolean properties, the tools have to make sure that .triggered is evaluated before the property even if .triggered is at a different clock (for the time steps where .triggered clock overlaps with property clock).

Manisha

_____________________________________________

From: Prabhakar, Anupam

Sent: Thursday, September 09, 2010 3:17 AM

To: john.havlicek@freescale.com

Cc: Kulshrestha, Manisha; Eduard.Cerny@synopsys.com

Subject: Mantis 2904

Hi John,

I was thinking about a good way to describe this. What I am concerned about is that simulators should not need to retract a 'boolean' type property after it has evaluated. For cases where sequence.triggered is used in a disable expression, and it is clocked with the same clock as that of the assertion, most simulators would ensure that the sequence.triggered is evaluated before the assertion. For cases when the clock is not same there can be a potential race condition when we can't do much and in my opinion we should leave this as is.

For

sequence s0; @(posedge clk) rst[*2]; endsequence

assert property (@(posedge clk) disable iff (s0.triggered) a|->b);

It is easy to ensure that s0.triggered evaluates before the assertion. Also, it should be always possible to determine a priority for evaluation of nested sequence.triggered as sequences cannot have cyclic dependency.

What do you think of this change ?

FROM

If prior to the completion of that evaluation the disable condition becomes true, then the overall evaluation of the property results in disabled. A property has disabled evaluation if it was preempted due to a disable iff condition.

TO

If prior to the completion of that evaluation the disable condition becomes true, then the overall evaluation of the property results in disabled. A property has disabled evaluation if it was preempted due to a disable iff condition. A new evaluation attempt for a property shall not start if the disable iff condition is true in the Observed region (in the time of occurrence of its leading clock event) and the property is considered to have a disabled evaluation for this time.

Anupam

--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.