******************************* huff.mv ******************************* vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> ROB4 huff vis> Class USUT ROB4 huff vis> character<0> 2 not protected character<1> 2 not protected character<2> 2 not protected character<3> 2 not protected character<4> 2 not protected character<5> 2 not protected character<6> 2 not protected character<7> 2 not protected decoder.state<0> 2 not protected decoder.state<1> 2 not protected decoder.state<2> 2 not protected decoder.state<3> 2 not protected decoder.state<4> 2 not protected decoder.state<5> 2 not protected decoder.state<6> 2 not protected decoder.state<7> 2 not protected decoder.state<8> 2 not protected decoder.state<9> 2 not protected encoder.shiftreg<0> 2 not protected encoder.shiftreg<1> 2 not protected encoder.shiftreg<2> 2 not protected encoder.shiftreg<3> 2 not protected encoder.shiftreg<4> 2 not protected encoder.shiftreg<5> 2 not protected encoder.shiftreg<6> 2 not protected encoder.shiftreg<7> 2 not protected encoder.shiftreg<8> 2 not protected encoder.shiftreg<9> 2 not protected ******************************** Error states = 2.243500e+04 States reachable from error states = 6.165400e+04 Reachable states whithout faults = 8.780000e+02 Analysis time = 0.5 vis> ******************************** Fair error states = 2.243500e+04 ******************************** Dealing with F = A[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 1.078500e+04 (Ratio: 4.807221e+01%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 0.25 ******************************** Dealing with F = E[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 2.243500e+04 (Ratio: 1.000000e+02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 0.04 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> Class USMT ROB4 huff vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> Class MSUT ROB4 huff vis> character<0> 2 not protected character<1> 2 not protected character<2> 2 not protected character<3> 2 not protected character<4> 2 not protected character<5> 2 not protected character<6> 2 not protected character<7> 2 not protected decoder.state<0> 2 not protected decoder.state<1> 2 not protected decoder.state<2> 2 not protected decoder.state<3> 2 not protected decoder.state<4> 2 not protected decoder.state<5> 2 not protected decoder.state<6> 2 not protected decoder.state<7> 2 not protected decoder.state<8> 2 not protected decoder.state<9> 2 not protected encoder.shiftreg<0> 2 not protected encoder.shiftreg<1> 2 not protected encoder.shiftreg<2> 2 not protected encoder.shiftreg<3> 2 not protected encoder.shiftreg<4> 2 not protected encoder.shiftreg<5> 2 not protected encoder.shiftreg<6> 2 not protected encoder.shiftreg<7> 2 not protected encoder.shiftreg<8> 2 not protected encoder.shiftreg<9> 2 not protected ******************************** Error states = 2.684355e+08 States reachable from error states = 2.684355e+08 Reachable states whithout faults = 8.780000e+02 Analysis time = 0.22 vis> ******************************** Fair error states = 2.684355e+08 ******************************** Dealing with F = A[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 1.898214e+07 (Ratio: 7.071400e+00%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 0.29 ******************************** Dealing with F = E[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 2.684355e+08 (Ratio: 1.000000e+02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 0.09 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> Class MSMT ROB4 huff vis> character<0> 2 not protected character<1> 2 not protected character<2> 2 not protected character<3> 2 not protected character<4> 2 not protected character<5> 2 not protected character<6> 2 not protected character<7> 2 not protected decoder.state<0> 2 not protected decoder.state<1> 2 not protected decoder.state<2> 2 not protected decoder.state<3> 2 not protected decoder.state<4> 2 not protected decoder.state<5> 2 not protected decoder.state<6> 2 not protected decoder.state<7> 2 not protected decoder.state<8> 2 not protected decoder.state<9> 2 not protected encoder.shiftreg<0> 2 not protected encoder.shiftreg<1> 2 not protected encoder.shiftreg<2> 2 not protected encoder.shiftreg<3> 2 not protected encoder.shiftreg<4> 2 not protected encoder.shiftreg<5> 2 not protected encoder.shiftreg<6> 2 not protected encoder.shiftreg<7> 2 not protected encoder.shiftreg<8> 2 not protected encoder.shiftreg<9> 2 not protected ******************************** Error states = 2.684355e+08 States reachable from error states = 2.684355e+08 Reachable states whithout faults = 8.780000e+02 Analysis time = 0.2 vis> ******************************** Fair error states = 2.684355e+08 ******************************** Dealing with F = A[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 1.898214e+07 (Ratio: 7.071400e+00%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 0.29 ******************************** Dealing with F = E[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 2.684355e+08 (Ratio: 1.000000e+02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 0.08 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> *** Rob3 *** Root main vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_golden.reg created (contains 28 registers) vis> ROB3 huff vis> Class USUT ROB3 huff vis> faulty.character<0> 2 not protected faulty.character<1> 2 not protected faulty.character<2> 2 not protected faulty.character<3> 2 not protected faulty.character<4> 2 not protected faulty.character<5> 2 not protected faulty.character<6> 2 not protected faulty.character<7> 2 not protected faulty.decoder.state<0> 2 not protected faulty.decoder.state<1> 2 not protected faulty.decoder.state<2> 2 not protected faulty.decoder.state<3> 2 not protected faulty.decoder.state<4> 2 not protected faulty.decoder.state<5> 2 not protected faulty.decoder.state<6> 2 not protected faulty.decoder.state<7> 2 not protected faulty.decoder.state<8> 2 not protected faulty.decoder.state<9> 2 not protected faulty.encoder.shiftreg<0> 2 not protected faulty.encoder.shiftreg<1> 2 not protected faulty.encoder.shiftreg<2> 2 not protected faulty.encoder.shiftreg<3> 2 not protected faulty.encoder.shiftreg<4> 2 not protected faulty.encoder.shiftreg<5> 2 not protected faulty.encoder.shiftreg<6> 2 not protected faulty.encoder.shiftreg<7> 2 not protected faulty.encoder.shiftreg<8> 2 not protected faulty.encoder.shiftreg<9> 2 not protected golden.character<0> 2 protected golden.character<1> 2 protected golden.character<2> 2 protected golden.character<3> 2 protected golden.character<4> 2 protected golden.character<5> 2 protected golden.character<6> 2 protected golden.character<7> 2 protected golden.decoder.state<0> 2 protected golden.decoder.state<1> 2 protected golden.decoder.state<2> 2 protected golden.decoder.state<3> 2 protected golden.decoder.state<4> 2 protected golden.decoder.state<5> 2 protected golden.decoder.state<6> 2 protected golden.decoder.state<7> 2 protected golden.decoder.state<8> 2 protected golden.decoder.state<9> 2 protected golden.encoder.shiftreg<0> 2 protected golden.encoder.shiftreg<1> 2 protected golden.encoder.shiftreg<2> 2 protected golden.encoder.shiftreg<3> 2 protected golden.encoder.shiftreg<4> 2 protected golden.encoder.shiftreg<5> 2 protected golden.encoder.shiftreg<6> 2 protected golden.encoder.shiftreg<7> 2 protected golden.encoder.shiftreg<8> 2 protected golden.encoder.shiftreg<9> 2 protected ******************************** Error states = 2.458400e+04 States reachable from error states = 1.425640e+06 Reachable states whithout faults = 8.780000e+02 Analysis time = 8.58 vis> ******************************** Fair error states = 2.458400e+04 ******************************** Dealing with F = A[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 1.102500e+04 (Ratio: 4.484624e+01%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 24.02 ******************************** Dealing with F = E[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 2.458400e+04 (Ratio: 1.000000e+02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 122.53 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> *** Rob3 *** Root main vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_golden.reg created (contains 28 registers) vis> Class MSUT ROB3 huff vis> faulty.character<0> 2 not protected faulty.character<1> 2 not protected faulty.character<2> 2 not protected faulty.character<3> 2 not protected faulty.character<4> 2 not protected faulty.character<5> 2 not protected faulty.character<6> 2 not protected faulty.character<7> 2 not protected faulty.decoder.state<0> 2 not protected faulty.decoder.state<1> 2 not protected faulty.decoder.state<2> 2 not protected faulty.decoder.state<3> 2 not protected faulty.decoder.state<4> 2 not protected faulty.decoder.state<5> 2 not protected faulty.decoder.state<6> 2 not protected faulty.decoder.state<7> 2 not protected faulty.decoder.state<8> 2 not protected faulty.decoder.state<9> 2 not protected faulty.encoder.shiftreg<0> 2 not protected faulty.encoder.shiftreg<1> 2 not protected faulty.encoder.shiftreg<2> 2 not protected faulty.encoder.shiftreg<3> 2 not protected faulty.encoder.shiftreg<4> 2 not protected faulty.encoder.shiftreg<5> 2 not protected faulty.encoder.shiftreg<6> 2 not protected faulty.encoder.shiftreg<7> 2 not protected faulty.encoder.shiftreg<8> 2 not protected faulty.encoder.shiftreg<9> 2 not protected golden.character<0> 2 protected golden.character<1> 2 protected golden.character<2> 2 protected golden.character<3> 2 protected golden.character<4> 2 protected golden.character<5> 2 protected golden.character<6> 2 protected golden.character<7> 2 protected golden.decoder.state<0> 2 protected golden.decoder.state<1> 2 protected golden.decoder.state<2> 2 protected golden.decoder.state<3> 2 protected golden.decoder.state<4> 2 protected golden.decoder.state<5> 2 protected golden.decoder.state<6> 2 protected golden.decoder.state<7> 2 protected golden.decoder.state<8> 2 protected golden.decoder.state<9> 2 protected golden.encoder.shiftreg<0> 2 protected golden.encoder.shiftreg<1> 2 protected golden.encoder.shiftreg<2> 2 protected golden.encoder.shiftreg<3> 2 protected golden.encoder.shiftreg<4> 2 protected golden.encoder.shiftreg<5> 2 protected golden.encoder.shiftreg<6> 2 protected golden.encoder.shiftreg<7> 2 protected golden.encoder.shiftreg<8> 2 protected golden.encoder.shiftreg<9> 2 protected ******************************** Error states = 2.356863e+11 States reachable from error states = 2.356863e+11 Reachable states whithout faults = 8.780000e+02 Analysis time = 1.51 vis> ******************************** Fair error states = 2.356863e+11 ******************************** Dealing with F = A[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 1.384898e+09 (Ratio: 5.876020e-01%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 8.32 ******************************** Dealing with F = E[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 2.356863e+11 (Ratio: 1.000000e+02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 103.11 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> *** Rob3 *** Root main vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_golden.reg created (contains 28 registers) vis> Class MSMT ROB3 huff vis> faulty.character<0> 2 not protected faulty.character<1> 2 not protected faulty.character<2> 2 not protected faulty.character<3> 2 not protected faulty.character<4> 2 not protected faulty.character<5> 2 not protected faulty.character<6> 2 not protected faulty.character<7> 2 not protected faulty.decoder.state<0> 2 not protected faulty.decoder.state<1> 2 not protected faulty.decoder.state<2> 2 not protected faulty.decoder.state<3> 2 not protected faulty.decoder.state<4> 2 not protected faulty.decoder.state<5> 2 not protected faulty.decoder.state<6> 2 not protected faulty.decoder.state<7> 2 not protected faulty.decoder.state<8> 2 not protected faulty.decoder.state<9> 2 not protected faulty.encoder.shiftreg<0> 2 not protected faulty.encoder.shiftreg<1> 2 not protected faulty.encoder.shiftreg<2> 2 not protected faulty.encoder.shiftreg<3> 2 not protected faulty.encoder.shiftreg<4> 2 not protected faulty.encoder.shiftreg<5> 2 not protected faulty.encoder.shiftreg<6> 2 not protected faulty.encoder.shiftreg<7> 2 not protected faulty.encoder.shiftreg<8> 2 not protected faulty.encoder.shiftreg<9> 2 not protected golden.character<0> 2 protected golden.character<1> 2 protected golden.character<2> 2 protected golden.character<3> 2 protected golden.character<4> 2 protected golden.character<5> 2 protected golden.character<6> 2 protected golden.character<7> 2 protected golden.decoder.state<0> 2 protected golden.decoder.state<1> 2 protected golden.decoder.state<2> 2 protected golden.decoder.state<3> 2 protected golden.decoder.state<4> 2 protected golden.decoder.state<5> 2 protected golden.decoder.state<6> 2 protected golden.decoder.state<7> 2 protected golden.decoder.state<8> 2 protected golden.decoder.state<9> 2 protected golden.encoder.shiftreg<0> 2 protected golden.encoder.shiftreg<1> 2 protected golden.encoder.shiftreg<2> 2 protected golden.encoder.shiftreg<3> 2 protected golden.encoder.shiftreg<4> 2 protected golden.encoder.shiftreg<5> 2 protected golden.encoder.shiftreg<6> 2 protected golden.encoder.shiftreg<7> 2 protected golden.encoder.shiftreg<8> 2 protected golden.encoder.shiftreg<9> 2 protected ******************************** Error states = 2.356863e+11 States reachable from error states = 2.356863e+11 Reachable states whithout faults = 8.780000e+02 Analysis time = 1.03 vis> ******************************** Fair error states = 2.356863e+11 ******************************** Dealing with F = A[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 1.384899e+09 (Ratio: 5.876024e-01%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 4.37 ******************************** Dealing with F = E[!forbiden U Required & A[!forbiden U Safe]] --Error states satisfying F = 2.356863e+11 (Ratio: 1.000000e+02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 119.79 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> *** Rob3 *** Root main vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_golden.reg created (contains 28 registers) vis> vis> ROB1 huff vis> Class USUT ROB1 huff vis> faulty.character<0> 2 not protected faulty.character<1> 2 not protected faulty.character<2> 2 not protected faulty.character<3> 2 not protected faulty.character<4> 2 not protected faulty.character<5> 2 not protected faulty.character<6> 2 not protected faulty.character<7> 2 not protected faulty.decoder.state<0> 2 not protected faulty.decoder.state<1> 2 not protected faulty.decoder.state<2> 2 not protected faulty.decoder.state<3> 2 not protected faulty.decoder.state<4> 2 not protected faulty.decoder.state<5> 2 not protected faulty.decoder.state<6> 2 not protected faulty.decoder.state<7> 2 not protected faulty.decoder.state<8> 2 not protected faulty.decoder.state<9> 2 not protected faulty.encoder.shiftreg<0> 2 not protected faulty.encoder.shiftreg<1> 2 not protected faulty.encoder.shiftreg<2> 2 not protected faulty.encoder.shiftreg<3> 2 not protected faulty.encoder.shiftreg<4> 2 not protected faulty.encoder.shiftreg<5> 2 not protected faulty.encoder.shiftreg<6> 2 not protected faulty.encoder.shiftreg<7> 2 not protected faulty.encoder.shiftreg<8> 2 not protected faulty.encoder.shiftreg<9> 2 not protected golden.character<0> 2 protected golden.character<1> 2 protected golden.character<2> 2 protected golden.character<3> 2 protected golden.character<4> 2 protected golden.character<5> 2 protected golden.character<6> 2 protected golden.character<7> 2 protected golden.decoder.state<0> 2 protected golden.decoder.state<1> 2 protected golden.decoder.state<2> 2 protected golden.decoder.state<3> 2 protected golden.decoder.state<4> 2 protected golden.decoder.state<5> 2 protected golden.decoder.state<6> 2 protected golden.decoder.state<7> 2 protected golden.decoder.state<8> 2 protected golden.decoder.state<9> 2 protected golden.encoder.shiftreg<0> 2 protected golden.encoder.shiftreg<1> 2 protected golden.encoder.shiftreg<2> 2 protected golden.encoder.shiftreg<3> 2 protected golden.encoder.shiftreg<4> 2 protected golden.encoder.shiftreg<5> 2 protected golden.encoder.shiftreg<6> 2 protected golden.encoder.shiftreg<7> 2 protected golden.encoder.shiftreg<8> 2 protected golden.encoder.shiftreg<9> 2 protected ******************************** Error states = 2.458400e+04 States reachable from error states = 1.425640e+06 Reachable states whithout faults = 8.780000e+02 Analysis time = 12.68 vis> ******************************** Fair error states = 2.458400e+04 ******************************** Dealing with F = AG[Safe]] --Error states satisfying F = 7.502000e+03 (Ratio: 3.051578e+01%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 28.57 ******************************** Dealing with F = EG[Safe]] --Error states satisfying F = 1.170700e+04 (Ratio: 4.762040e+01%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 33.9 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> *** Rob3 *** Root main vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_golden.reg created (contains 28 registers) vis> vis> Class MSUT ROB1 huff vis> faulty.character<0> 2 not protected faulty.character<1> 2 not protected faulty.character<2> 2 not protected faulty.character<3> 2 not protected faulty.character<4> 2 not protected faulty.character<5> 2 not protected faulty.character<6> 2 not protected faulty.character<7> 2 not protected faulty.decoder.state<0> 2 not protected faulty.decoder.state<1> 2 not protected faulty.decoder.state<2> 2 not protected faulty.decoder.state<3> 2 not protected faulty.decoder.state<4> 2 not protected faulty.decoder.state<5> 2 not protected faulty.decoder.state<6> 2 not protected faulty.decoder.state<7> 2 not protected faulty.decoder.state<8> 2 not protected faulty.decoder.state<9> 2 not protected faulty.encoder.shiftreg<0> 2 not protected faulty.encoder.shiftreg<1> 2 not protected faulty.encoder.shiftreg<2> 2 not protected faulty.encoder.shiftreg<3> 2 not protected faulty.encoder.shiftreg<4> 2 not protected faulty.encoder.shiftreg<5> 2 not protected faulty.encoder.shiftreg<6> 2 not protected faulty.encoder.shiftreg<7> 2 not protected faulty.encoder.shiftreg<8> 2 not protected faulty.encoder.shiftreg<9> 2 not protected golden.character<0> 2 protected golden.character<1> 2 protected golden.character<2> 2 protected golden.character<3> 2 protected golden.character<4> 2 protected golden.character<5> 2 protected golden.character<6> 2 protected golden.character<7> 2 protected golden.decoder.state<0> 2 protected golden.decoder.state<1> 2 protected golden.decoder.state<2> 2 protected golden.decoder.state<3> 2 protected golden.decoder.state<4> 2 protected golden.decoder.state<5> 2 protected golden.decoder.state<6> 2 protected golden.decoder.state<7> 2 protected golden.decoder.state<8> 2 protected golden.decoder.state<9> 2 protected golden.encoder.shiftreg<0> 2 protected golden.encoder.shiftreg<1> 2 protected golden.encoder.shiftreg<2> 2 protected golden.encoder.shiftreg<3> 2 protected golden.encoder.shiftreg<4> 2 protected golden.encoder.shiftreg<5> 2 protected golden.encoder.shiftreg<6> 2 protected golden.encoder.shiftreg<7> 2 protected golden.encoder.shiftreg<8> 2 protected golden.encoder.shiftreg<9> 2 protected ******************************** Error states = 2.356863e+11 States reachable from error states = 2.356863e+11 Reachable states whithout faults = 8.780000e+02 Analysis time = 1.11 vis> ******************************** Fair error states = 2.356863e+11 ******************************** Dealing with F = AG[Safe]] --Error states satisfying F = 1.449618e+06 (Ratio: 6.150624e-04%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 29.27 ******************************** Dealing with F = EG[Safe]] --Error states satisfying F = 5.338613e+07 (Ratio: 2.265135e-02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 4.27 vis> vis release 2.3 (compiled 13-Jul-11 at 10:56 AM) vis> vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_output created (contains 8 signals) vis> *** Rob3 *** Root main vis> vis> Dynamic variable ordering is enabled with method sift. vis> file protect_golden.reg created (contains 28 registers) vis> vis> Class MSMT ROB1 huff vis> faulty.character<0> 2 not protected faulty.character<1> 2 not protected faulty.character<2> 2 not protected faulty.character<3> 2 not protected faulty.character<4> 2 not protected faulty.character<5> 2 not protected faulty.character<6> 2 not protected faulty.character<7> 2 not protected faulty.decoder.state<0> 2 not protected faulty.decoder.state<1> 2 not protected faulty.decoder.state<2> 2 not protected faulty.decoder.state<3> 2 not protected faulty.decoder.state<4> 2 not protected faulty.decoder.state<5> 2 not protected faulty.decoder.state<6> 2 not protected faulty.decoder.state<7> 2 not protected faulty.decoder.state<8> 2 not protected faulty.decoder.state<9> 2 not protected faulty.encoder.shiftreg<0> 2 not protected faulty.encoder.shiftreg<1> 2 not protected faulty.encoder.shiftreg<2> 2 not protected faulty.encoder.shiftreg<3> 2 not protected faulty.encoder.shiftreg<4> 2 not protected faulty.encoder.shiftreg<5> 2 not protected faulty.encoder.shiftreg<6> 2 not protected faulty.encoder.shiftreg<7> 2 not protected faulty.encoder.shiftreg<8> 2 not protected faulty.encoder.shiftreg<9> 2 not protected golden.character<0> 2 protected golden.character<1> 2 protected golden.character<2> 2 protected golden.character<3> 2 protected golden.character<4> 2 protected golden.character<5> 2 protected golden.character<6> 2 protected golden.character<7> 2 protected golden.decoder.state<0> 2 protected golden.decoder.state<1> 2 protected golden.decoder.state<2> 2 protected golden.decoder.state<3> 2 protected golden.decoder.state<4> 2 protected golden.decoder.state<5> 2 protected golden.decoder.state<6> 2 protected golden.decoder.state<7> 2 protected golden.decoder.state<8> 2 protected golden.decoder.state<9> 2 protected golden.encoder.shiftreg<0> 2 protected golden.encoder.shiftreg<1> 2 protected golden.encoder.shiftreg<2> 2 protected golden.encoder.shiftreg<3> 2 protected golden.encoder.shiftreg<4> 2 protected golden.encoder.shiftreg<5> 2 protected golden.encoder.shiftreg<6> 2 protected golden.encoder.shiftreg<7> 2 protected golden.encoder.shiftreg<8> 2 protected golden.encoder.shiftreg<9> 2 protected ******************************** Error states = 2.356863e+11 States reachable from error states = 2.356863e+11 Reachable states whithout faults = 8.780000e+02 Analysis time = 0.96 vis> ******************************** Fair error states = 2.356863e+11 ******************************** Dealing with F = AG[Safe]] --Error states satisfying F = 1.450496e+06 (Ratio: 6.154349e-04%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 24.5 ******************************** Dealing with F = EG[Safe]] --Error states satisfying F = 5.338701e+07 (Ratio: 2.265172e-02%) --Error states originaly reachable by the design and satisfying F = 8.780000e+02 (Ratio: 1.000000e+02%) Analysis time = 29.62