// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // macro NumProc = 10; module Arbiter([NumProc]bool ?req, event bool ?rdy, [NumProc]bool ack, tok, prs, bool arb, bool static) { loop{ for (i=0 .. (NumProc-1)) do || { next(tok[i]) = true; await (arb); next(tok[i]) = false; } } || for (i=0 .. (NumProc-1)) do || loop { await (req[i] & tok[i]); next(prs[i]) = true; await (not req[i]); next(prs[i]) = false; } || loop { arb = true; await(exists(i=0 .. (NumProc-1)) req[i]); arb = false; static = not exists(i=0 .. (NumProc-1)) (prs[i] & tok[i]); if (not(static)) for (i = (NumProc-1) .. 0) do || { if (req[i] & tok[i] & prs[i] & forall (j=i..(NumProc-1)) ack[j]==false) ack[i] = true; } else { for (i=NumProc .. 0) do || { if (req[i] & forall(j=i..(NumProc)) (req[j]==false)) ack[i] = true; } } wfa : await (rdy); } }