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

GLOBAL {
  PARAMETERS {
    n = 12;
  }

  DEFINITIONS {
    /* Checks whether a bus of size log(n) currently represents 
     * the numerical value v (encoded in binary).
     */
    value(bus,v) = value'(bus,v,0,SIZEOF bus);
    value'(bus,v,i,j) =
      i >= j        : true
      bit(v,i) == 1 : value'(bus,v,i + 1,j) &&  bus[i]
      othe

... [truncated 1.2 kB]

ASSUMPTIONS {
    // at every time exactely one grant is HIGH
    G mutual_exclusion(HGRANT);
    G (||[0 <= i < n] HGRANT[i]);
  }

  INVARIANTS {
    // the component outputs the binary encoding i of the i-th,
    // whenever i is granted and HREADY is high
    &&[0 <= i < n] (HREADY -> (X value(HMASTER,i) <-> HGRANT[i]));

    // when HREADY is low it copies the old value
    !HREADY -> (&&[0 <= i < log2(n-1)] (X HMASTER[i] <-> HMASTER[i]));
  }
}
//#!SYNTCOMP
//STATUS : realizable
//REF_SIZE : 307
//#.