[sv-ac] 1757 resets - proposal from 071024.

Hi Doron,

Finally I got to reading the proposal again. Questions:

pp342, item h: It says "If prior to the completion of that evaluation
the disable condition becomes true, then the overall evaluation of the
property results in true."

Similarly for reject_on. To me "prior" means strictly before. Yet in
16.12.3 it says:
"When the disable condition occurs at the same time step where the
evaluation of the property_expr ends, the disable condition takes
precedence."

Should the first sentence be changed? 
Also, the sentence says "disable condition", but it defined the two
operators as resets. Should this be called reset condition?

Similarly in the subsequent examples:
"For example,

property p; (accept_on(a) p1) and (reject_on(b) p2); endproperty
If a becomes true before the evaluation ofp1is completed and the
second term of the and operation
completed evaluation, the truth ofp1is ignored in deciding the truth
ofpOn the other hand, ifbbecomes
true before the evaluation of p2 is completed thenpevaluates to false.
"
Should it say "If a becomes true before or in the same time step when
the evaluation of p1 is completed..." ? 

Similarly the other examples?

Best regards,
ed






-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.