[sv-ac] Issue with Mantis 2722. Further discussion

Looking at this example closer, I think it should be rewritten in a more radical manner. The statement "Each time the sequence $rose(data_phase) matches, an evaluation of the consequent property begins." is incorrect. The property evaluation begins depending on its position in an assertion. E.g., if I write assert property (cond |-> data_end) then the evaluation of data_end begins only when cond is evaluated to true. If cond is always false the evaluation of data_end never begins. I think we need to wrap this property data_end into an assertion:

assert property(data_end);

Then the (modified) language in the example will be correct. Another option is to state that the attempt of data_end is successful at this point. The same applies to subsequent examples as well.

Thanks,
Dmitry

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
Sent: Wednesday, May 11, 2011 23:05
To: 'sv-ac@eda-stds.org'
Subject: [sv-ac] Issue with Mantis 2722

Hi all,

I don't like the description in Mantis 2722: "Then, at clock tick 6, data_end evaluates to true because $fell(stop) and irdy==0 both evaluate to true." Though, formally speaking this sentence is correct, it is correct "vacuously". The property evaluates to true or false at its beginning. E.g., the property $rose(data_phase) |-> ##[1,5] ((irdy==0) && ($fell(trdy) || $fell(stop))) evaluates to true at time 2 since $rose(data_phase) is true at time 2, and ((irdy==0) && ($fell(trdy) || $fell(stop))) is true at time 6 (Fig. 16-14). What we intended to say that at clock tick 6, data_end is detected to be true. $rose(data_phase) |-> ##[1,5] ((irdy==0) && ($fell(trdy) || $fell(stop))) is indeed true at time 6, but only due to $rose(data_phase) is false at that time.

I suggest we change "evaluates to true" to "is detected to be true".

What do you think?

Thanks,
Dmitry
---------------------------------------------------------------------
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<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.