#FAIL: a specified reset state must eventually be reached from every state.
# This formula fails in spite of the fairness conditions.
G(F(min[8:0]=b111111111 * last[8:0]=0 * max[8:0]=0));

#PASS: The non-reset states reachable in one clock cycle from the reset
# states have min == last == max.
G(min[8:0]=b111111111 * max[8:0]=b000000000 ->
  X(min[8:0]=b111111111 * max[8:0]=b000000000 +
    min[8:0] == last[8:0] * last[8:0] == max[8:0]));

#PASS: The non-reset states reachable in two clock cycles from the reset
# states have either min == last or last == max.
G(min[8:0]=b111111111 * max[8:0]=b000000000 ->
  X:2(min[8:0]=b111111111 * max[8:0]=b000000000 +
      min[8:0] == last[8:0] + last[8:0] == max[8:0]));