#PASS: a specified reset state can eventually be reached from every
# reachable state.

AG(EF(min[29:0]=b111111111111111111111111111111 * last[29:0]=0 * max[29:0]=0));