[sv-ac] clock flow rules for until next

Hi John,

 

      I took an action item to review the clock flow.

 

*	The semantics for  @(c1)<next>Q is that Q is being evaluated
staring from the second accordance of c1.

In particular, if c1 occurs at the current time, then Q is being
evaluated in the strictly next time that c1 occurs.

 

      I think that it makes sense because the first occurrence of c1 is
where the evaluation of <next>Q starts

 

*	The semantics of @(c1) (Q1 <until> Q2) is there should be an
occurrence of c1 where Q2 holds, and in every 

       occurrence of c1 before that, Q1 holds.

      

             That also makes sense to me

 

Doron

 

 

  


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