*** 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