mux.tlsf

INFO {
  TITLE:       "n-ary mux"
  DESCRIPTION: "selects the output out of a set of inputs according to a given
 binary encoded input"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

GLOBAL {
  PARAMETERS {
    n = 10;
  }

  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]
      otherwise     : value'(bus,v,i + 1,j) && !bus[i];

    /* Returns the i-th bit of the numerical value v. */
    bit(v,i) =
      i <= 0     : v % 2
      otherwise  : bit(v / 2,i - 1);

    /* floor(log2) */
    log2_dn(x) =
      x <= 1    : 0
      otherwise : 1 + log2_dn(x/2);

    /* nbits(x): return the number of bits needed to encode x values
     * This is similar to ceil(log2) except for value 1: nbits(1) = 1 while ceil(log2(1)) = 0
    */
    nbits(x) =
      x == 0    : 0
      otherwise : 1 + log2_dn(x-1);
  }
}

MAIN {
  INPUTS {
    select[nbits(n)];
    in[n];
  }

  OUTPUTS {
    out;
  }

  ASSERT {
    &&[0 <= i < n]
      (value(select,i) -> out <-> in[i]);
  }
}