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