*** This is NuSMV 2.3.1 (compiled on Mon Nov 21 15:48:12 UTC 2005) *** For more information on NuSMV see *** or email to . *** Please report bugs to . WARNING *** This version of NuSMV is linked to the MiniSat SAT solver *** WARNING *** See http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat *** WARNING *** Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson *** WARNING *** MiniSat is used in Bounded Model Checking when the *** WARNING *** environment variable sat_solver is set to 'minisat'. *** WARNING *** THE SOFTWARE IS PROVIDED 'AS IS', WITHOUT WARRANTY OF ANY KIND, *** WARNING *** EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES *** WARNING *** OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND *** WARNING *** NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT *** WARNING *** HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, *** WARNING *** WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *** WARNING *** FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR *** WARNING *** OTHER DEALINGS IN THE SOFTWARE. *** Starting the batch interaction. Parsing file /workspace/gabe/AMBA_AHB_Performance_Evaluation_128x128_Tiles.smv ......done. Flattening hierarchy ......done. Encoding variables ...... done. Building Model ...checking for multiple assignments... Done checking for circular assignments... Done ... done. ... done. evaluating specification AG (START4 -> TIME < 170) Computing the set of fair x pairs size of res0 = 1.18059e+21 x, 1 BDD nodes size of res1 = 2.31667e+15 x, 2892 BDD nodes done eu: computing fixed point approximations for AG (START4 -> TIME < 170) ... size of Y1 = 4.52475e+12 states, 5764 BDD nodes size of Y2 = 4.7352e+12 states, 6034 BDD nodes size of Y3 = 4.94565e+12 states, 6270 BDD nodes size of Y4 = 5.05088e+12 states, 6272 BDD nodes size of Y5 = 5.07719e+12 states, 6558 BDD nodes size of Y6 = 5.11082e+12 states, 7290 BDD nodes size of Y7 = 5.14642e+12 states, 7991 BDD nodes size of Y8 = 5.18035e+12 states, 8479 BDD nodes size of Y9 = 5.20062e+12 states, 8639 BDD nodes size of Y10 = 5.21002e+12 states, 9223 BDD nodes size of Y11 = 5.22205e+12 states, 9905 BDD nodes size of Y12 = 5.24486e+12 states, 10038 BDD nodes size of Y13 = 5.2683e+12 states, 10148 BDD nodes size of Y14 = 5.28392e+12 states, 10150 BDD nodes size of Y15 = 5.29315e+12 states, 10330 BDD nodes size of Y16 = 5.30106e+12 states, 10532 BDD nodes size of Y17 = 5.30983e+12 states, 10596 BDD nodes size of Y18 = 5.31874e+12 states, 10799 BDD nodes size of Y19 = 5.32695e+12 states, 11031 BDD nodes size of Y20 = 5.33461e+12 states, 11177 BDD nodes size of Y21 = 5.34215e+12 states, 11218 BDD nodes size of Y22 = 5.34996e+12 states, 11233 BDD nodes size of Y23 = 5.35778e+12 states, 11392 BDD nodes size of Y24 = 5.36546e+12 states, 11519 BDD nodes size of Y25 = 5.37302e+12 states, 11629 BDD nodes size of Y26 = 5.38055e+12 states, 11722 BDD nodes size of Y27 = 5.38809e+12 states, 11788 BDD nodes size of Y28 = 5.39565e+12 states, 11906 BDD nodes size of Y29 = 5.4032e+12 states, 12032 BDD nodes size of Y30 = 5.41117e+12 states, 12164 BDD nodes size of Y31 = 5.42249e+12 states, 12310 BDD nodes size of Y32 = 5.43546e+12 states, 12412 BDD nodes size of Y33 = 5.44927e+12 states, 12524 BDD nodes size of Y34 = 5.4633e+12 states, 12631 BDD nodes size of Y35 = 5.47757e+12 states, 12751 BDD nodes size of Y36 = 5.49197e+12 states, 12828 BDD nodes size of Y37 = 5.50646e+12 states, 12911 BDD nodes size of Y38 = 5.52092e+12 states, 12991 BDD nodes size of Y39 = 5.5353e+12 states, 13071 BDD nodes size of Y40 = 5.54966e+12 states, 13135 BDD nodes size of Y41 = 5.5641e+12 states, 13201 BDD nodes size of Y42 = 5.58052e+12 states, 13162 BDD nodes size of Y43 = 5.59589e+12 states, 13254 BDD nodes size of Y44 = 5.61103e+12 states, 13306 BDD nodes size of Y45 = 5.62589e+12 states, 13377 BDD nodes size of Y46 = 5.64082e+12 states, 13493 BDD nodes size of Y47 = 5.65614e+12 states, 13517 BDD nodes size of Y48 = 5.67166e+12 states, 13462 BDD nodes size of Y49 = 5.68693e+12 states, 13376 BDD nodes size of Y50 = 5.70254e+12 states, 13290 BDD nodes size of Y51 = 5.71746e+12 states, 13287 BDD nodes size of Y52 = 5.73236e+12 states, 13217 BDD nodes size of Y53 = 5.74727e+12 states, 13095 BDD nodes size of Y54 = 5.76218e+12 states, 13136 BDD nodes size of Y55 = 5.77705e+12 states, 13173 BDD nodes size of Y56 = 5.79188e+12 states, 13169 BDD nodes size of Y57 = 5.80671e+12 states, 12954 BDD nodes size of Y58 = 5.82154e+12 states, 12880 BDD nodes size of Y59 = 5.83636e+12 states, 12895 BDD nodes size of Y60 = 5.85119e+12 states, 12887 BDD nodes size of Y61 = 5.86602e+12 states, 12830 BDD nodes size of Y62 = 5.88043e+12 states, 12685 BDD nodes size of Y63 = 5.8914e+12 states, 12703 BDD nodes size of Y64 = 5.90072e+12 states, 12682 BDD nodes size of Y65 = 5.90921e+12 states, 12815 BDD nodes size of Y66 = 5.91751e+12 states, 12788 BDD nodes size of Y67 = 5.92557e+12 states, 12784 BDD nodes size of Y68 = 5.93352e+12 states, 12747 BDD nodes size of Y69 = 5.94136e+12 states, 12722 BDD nodes size of Y70 = 5.94914e+12 states, 12681 BDD nodes size of Y71 = 5.95691e+12 states, 12659 BDD nodes size of Y72 = 5.96466e+12 states, 12608 BDD nodes size of Y73 = 5.97231e+12 states, 12574 BDD nodes size of Y74 = 5.97986e+12 states, 12528 BDD nodes size of Y75 = 5.98736e+12 states, 12501 BDD nodes size of Y76 = 5.99484e+12 states, 12447 BDD nodes size of Y77 = 6.00232e+12 states, 12370 BDD nodes size of Y78 = 6.0098e+12 states, 12291 BDD nodes size of Y79 = 6.01727e+12 states, 12259 BDD nodes size of Y80 = 6.02474e+12 states, 12152 BDD nodes size of Y81 = 6.03221e+12 states, 12069 BDD nodes size of Y82 = 6.03967e+12 states, 11938 BDD nodes size of Y83 = 6.04716e+12 states, 11744 BDD nodes size of Y84 = 6.05462e+12 states, 11700 BDD nodes size of Y85 = 6.06207e+12 states, 11669 BDD nodes size of Y86 = 6.06953e+12 states, 11613 BDD nodes size of Y87 = 6.07698e+12 states, 11596 BDD nodes size of Y88 = 6.08443e+12 states, 11589 BDD nodes size of Y89 = 6.09188e+12 states, 11590 BDD nodes size of Y90 = 6.09933e+12 states, 11584 BDD nodes size of Y91 = 6.10678e+12 states, 11597 BDD nodes size of Y92 = 6.11422e+12 states, 11590 BDD nodes size of Y93 = 6.12167e+12 states, 11298 BDD nodes size of Y94 = 6.1287e+12 states, 11050 BDD nodes size of Y95 = 6.13227e+12 states, 11049 BDD nodes size of Y96 = 6.13419e+12 states, 10750 BDD nodes size of Y97 = 6.13529e+12 states, 10455 BDD nodes size of Y98 = 6.13619e+12 states, 10023 BDD nodes size of Y99 = 6.20341e+12 states, 10248 BDD nodes size of Y100 = 6.22514e+12 states, 10343 BDD nodes size of Y101 = 6.23965e+12 states, 10382 BDD nodes size of Y102 = 6.24516e+12 states, 10487 BDD nodes size of Y103 = 6.25311e+12 states, 10992 BDD nodes size of Y104 = 6.26974e+12 states, 11082 BDD nodes size of Y105 = 6.29228e+12 states, 11206 BDD nodes size of Y106 = 6.30553e+12 states, 11090 BDD nodes size of Y107 = 6.31069e+12 states, 11045 BDD nodes size of Y108 = 6.31543e+12 states, 11166 BDD nodes size of Y109 = 6.31898e+12 states, 11198 BDD nodes size of Y110 = 6.32161e+12 states, 11028 BDD nodes size of Y111 = 6.32364e+12 states, 10899 BDD nodes size of Y112 = 6.32475e+12 states, 10676 BDD nodes size of Y113 = 6.32566e+12 states, 10589 BDD nodes size of Y114 = 6.32679e+12 states, 10453 BDD nodes size of Y115 = 6.32791e+12 states, 10362 BDD nodes size of Y116 = 6.32882e+12 states, 10273 BDD nodes size of Y117 = 6.32946e+12 states, 10212 BDD nodes size of Y118 = 6.33001e+12 states, 10157 BDD nodes size of Y119 = 6.33051e+12 states, 10146 BDD nodes size of Y120 = 6.33099e+12 states, 10113 BDD nodes size of Y121 = 6.33146e+12 states, 10083 BDD nodes size of Y122 = 6.33193e+12 states, 10048 BDD nodes size of Y123 = 6.3324e+12 states, 10024 BDD nodes size of Y124 = 6.33287e+12 states, 9990 BDD nodes size of Y125 = 6.33333e+12 states, 9958 BDD nodes size of Y126 = 6.3338e+12 states, 9922 BDD nodes size of Y127 = 6.33426e+12 states, 9888 BDD nodes size of Y128 = 6.33472e+12 states, 9712 BDD nodes size of Y129 = 6.33517e+12 states, 9521 BDD nodes size of Y130 = 6.33554e+12 states, 9427 BDD nodes size of Y131 = 6.33575e+12 states, 9258 BDD nodes size of Y132 = 6.33587e+12 states, 9051 BDD nodes size of Y133 = 6.33596e+12 states, 8798 BDD nodes size of Y134 = 6.3363e+12 states, 8633 BDD nodes size of Y135 = 6.33949e+12 states, 8757 BDD nodes size of Y136 = 6.3402e+12 states, 8682 BDD nodes size of Y137 = 6.34066e+12 states, 8601 BDD nodes size of Y138 = 6.34103e+12 states, 8484 BDD nodes size of Y139 = 6.34166e+12 states, 8256 BDD nodes size of Y140 = 6.34237e+12 states, 8094 BDD nodes size of Y141 = 6.34325e+12 states, 8045 BDD nodes size of Y142 = 6.3437e+12 states, 7850 BDD nodes size of Y143 = 6.3441e+12 states, 7740 BDD nodes size of Y144 = 6.34424e+12 states, 7587 BDD nodes size of Y145 = 6.34434e+12 states, 7465 BDD nodes size of Y146 = 6.34434e+12 states, 7375 BDD nodes -- specification AG (START4 -> TIME < 170) is true ###################################################################### Runtime Statistics ------------------ Machine name: node-xeon-9 User time 61.440 seconds System time 0.050 seconds Average resident text size = 0K Average resident data+stack size = 0K Maximum resident size = 0K Virtual text size = 132044K Virtual data size = 11793K data size initialized = 234K data size uninitialized = 362K data size sbrk = 11197K Virtual memory limit = 4194304K (4194304K) Major page faults = 411 Minor page faults = 4907 Swaps = 0 Input blocks = 0 Output blocks = 0 Context switch (voluntary) = 0 Context switch (involuntary) = 0 ###################################################################### BDD statistics -------------------- BDD nodes allocated: 69658 -------------------- BDD nodes representing init set of states: 28 BDD nodes representing state constraints: 2892 BDD nodes representing input constraints: 1 Forward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 3538 cluster 2 : 1505 Backward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 3538 cluster 2 : 1505