Monitor Example

Monitor Example

Property: If A requests resource, and resource is free, A gets resource within 3 clock cycles unless another client requests resource in the meantime.

Bad Behavior: For more than 3 clock cycles,

A is in state REQ and ackA is false,

B and C are in state NO REQ.

Monitor:

assign not_served = (A.state = REQ) && !(ackA) &&

(B.state != REQ) && (C.state != REQ)

Previous slide

Next slide

Back to the first slide

View Graphic Version