INFO {
  TITLE:       "Amba AHB - Decomposed - Arbiter"
  DESCRIPTION: "Arbiter component of the decomposed Amba AHB Arbiter"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

GLOBAL {
  PARAMETERS {
    n = 4;
  }

  DEFINITIONS {
    // ensures mutual exclusion on an n-ary bus
    mutual_exclusion(bus) =
     mone(bus,0,(SIZEOF bus) - 1);

    // ensures that none of the signals
    // bus[i] - bus[j] is HIGH
    none(bus,i,j) =
      &&[i <= t <= j]
        !bus[t];

    // ensures that at most one of the sig

... [truncated 1.2 kB]

] -> (BUSREQ <-> HBUSREQ[i]));

    // decisions can only be taken when the component is ready
    !ALLREADY -> !DECIDE;

    // the DECIDE signal marks when another master is granted in the
    // next step
    DECIDE <-> (||[0 <= i < n] !(X HGRANT[i] <-> HGRANT[i]));

    // if there are no requests master 0 is granted
    (&&[0 <= i < n] !HBUSREQ[i]) && DECIDE -> X HGRANT[0];
  }

  GUARANTEES {
    // initial values
    !DECIDE && HGRANT[0];
  }
}
//#!SYNTCOMP
//STATUS : realizable
//REF_SIZE : 68
//#.