[CST-2] Spec&Ver2: CTL

[Matthew Richards]

> (a) if req goes high then it will stay high until ack goes high and then
> go low on the next cycle [2 marks]

> AG(req => (A[req U ack] &
>    ack => req & AX(~req) )

I'm not quite sure about this - assuming there's supposed to be an extra
closing bracket at the end, it doesn't seem to cover the case where req goes
low at the same time as ack goes high - ignoring the A[req U ack] bit it
says

AG(req => ack => req & AX(~req))

which (apart from having a redundant req) doesn't do quite the right 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.

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?

>
> (b)
> AG(req & ~started => AF(AG error))

Sounds right to me.


Matthew