[CST-2] Spec&Ver2: CTL

[M.Y.W.Y. Becker]

--On 01 June 2001 22:17 +0100 Matthew Richards <mwr22@cam.ac.uk> wrote:
[...]
> thing. Alternatively, if you missed a bracket at the end of the first
> line:
>
> AG(req => (A[req U ack]) &
>    ack => req & AX(~req) )
>
> that doesn't cover it either - it requires that ack always forces req low,
> which is not necessarily true.

Yes, I meant this alternative, and you're right, it's wrong.


> The one I came up with is rather ugly, and may well have bugs:
>
> AG(req =>  ( A[req U ack]
>            & A[~ack U (req & AX(~req))] ))
>
> In other words (once req goes high), req is high until ack goes high, and
> ack doesn't go high until req is going to go low on the next cycle.  Does
> it look ok?

Looks correct, so far... but it does look quite ugly for just 2 marks...

Mo