RGD Arbiter

Specifications

Informal

an RGD Arbiter has four input terminals (r_0, d_0, r_1, and d_1) and two output terminals (g_0 and g_1). For each i in {0,1}, signaling starts with r_i followed by a repetition of g_i then concurrently d_i and r_i. The intervals from g_0 to d_0 and from g_1 to d_1 are mutually exclusive (do not overlap).

RGD stands for Request (r_i), Grant (g_i), and Done (d_i).

When An RGD Arbiter receives two requests, it will grant exactly one of them (and delay the other). The specification leaves the choice open. Often there is a fairness requirement on this choice: if a choice situation arises `infinitely often' then both outputs are chosen `infinitely often'.

XDI

Schematic diagram for an RGD Arbiter:

[Zoom|FIG]

XDI state graph for an RGD Arbiter:

[Zoom|FIG]

Specification in XDI model.

Verdect

Specification in Verdect:


define RGD( r0?, g0!, d0?, r1?, g1!, d1? ) =
       pref *[ r0?; g0!; ]
   ||  pref *[ r1?; g1!; ]
   ||  pref *[ g0!; d0? | g1!; d1? ]
end

Also available through this link

DI Algebra

Specification in DI Algebra:

NAME = (RGD Arbiter)
I = { r0, d0, r1, d1 }
O = { g0, g1 }

RGD = [ r0? -> g0! ; [ d0? -> RGD, d1? -> CHAOS ],
        r1? -> g1! ; [ d1? -> RGD, d0? -> CHAOS ],
        d0? -> CHAOS, d1? -> CHAOS
      ]
.

Also available through this link