INFO {
  TITLE:       "Amba AHB - Decomposed - Lock"
  DESCRIPTION: "Lock 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]
      otherwis

... [truncated 991 Bytes]

MAIN {
  INPUTS {
    DECIDE;
    HGRANT[n];
    HLOCK[n];
  } 

  OUTPUTS {
    LOCKED;
  }

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

  INVARIANTS {
    // whenever a decicion is taken, the LOCKED signal is updated to
    // the HLOCK value of the granted master
    &&[0 <= i < n] (DECIDE && X HGRANT[i] -> (X LOCKED <-> X HLOCK[i]));

    // otherwise the value is copied
    !DECIDE -> (X LOCKED <-> LOCKED)
  }
}