[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, and is
believed to be clean.