*** 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_Functional_Verification_3Masters_Correct.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 master1.state != error Computing the set of fair x pairs size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16818 BDD nodes size of Y2 = 5.90296e+20 x, 8816 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 8025 BDD nodes size of res1 = 2.26774e+13 x, 8806 BDD nodes size of Y0 = 7.97146e+12 x, 8024 BDD nodes size of Y1 = 1.93102e+13 x, 16808 BDD nodes size of Y2 = 2.26774e+13 x, 8806 BDD nodes size of Y0 = 1.4706e+13 x, 8798 BDD nodes size of Y1 = 2.26774e+13 x, 8806 BDD nodes done eu: computing fixed point approximations for AG master1.state != error ... size of Y1 = 2.83468e+12 states, 4702 BDD nodes size of Y2 = 1.49873e+13 states, 10643 BDD nodes size of Y3 = 1.7259e+13 states, 11889 BDD nodes size of Y4 = 1.77096e+13 states, 20092 BDD nodes size of Y5 = 1.8092e+13 states, 44057 BDD nodes size of Y6 = 1.85947e+13 states, 69380 BDD nodes size of Y7 = 1.90362e+13 states, 99681 BDD nodes size of Y8 = 1.92708e+13 states, 126447 BDD nodes size of Y9 = 1.94137e+13 states, 123568 BDD nodes size of Y10 = 1.94844e+13 states, 101476 BDD nodes size of Y11 = 1.95154e+13 states, 92792 BDD nodes size of Y12 = 1.95247e+13 states, 87228 BDD nodes size of Y13 = 1.95286e+13 states, 79914 BDD nodes size of Y14 = 1.95302e+13 states, 73085 BDD nodes size of Y15 = 1.95308e+13 states, 68721 BDD nodes size of Y16 = 1.95309e+13 states, 66365 BDD nodes size of Y17 = 1.95309e+13 states, 65958 BDD nodes -- specification AG master1.state != error is true evaluating specification AG master2.state != error eu: computing fixed point approximations for AG master2.state != error ... size of Y1 = 2.83468e+12 states, 3846 BDD nodes size of Y2 = 1.49873e+13 states, 13966 BDD nodes size of Y3 = 1.7259e+13 states, 13608 BDD nodes size of Y4 = 1.77096e+13 states, 21721 BDD nodes size of Y5 = 1.8092e+13 states, 47887 BDD nodes size of Y6 = 1.85947e+13 states, 79230 BDD nodes size of Y7 = 1.90362e+13 states, 110328 BDD nodes size of Y8 = 1.92708e+13 states, 134115 BDD nodes size of Y9 = 1.94137e+13 states, 130628 BDD nodes size of Y10 = 1.94844e+13 states, 108609 BDD nodes size of Y11 = 1.95154e+13 states, 98430 BDD nodes size of Y12 = 1.95247e+13 states, 91454 BDD nodes size of Y13 = 1.95286e+13 states, 84222 BDD nodes size of Y14 = 1.95302e+13 states, 78631 BDD nodes size of Y15 = 1.95308e+13 states, 73573 BDD nodes size of Y16 = 1.95309e+13 states, 71294 BDD nodes size of Y17 = 1.95309e+13 states, 70831 BDD nodes -- specification AG master2.state != error is true evaluating specification AG master3.state != error eu: computing fixed point approximations for AG master3.state != error ... size of Y1 = 2.83468e+12 states, 3490 BDD nodes size of Y2 = 1.49873e+13 states, 15175 BDD nodes size of Y3 = 1.7259e+13 states, 14235 BDD nodes size of Y4 = 1.77096e+13 states, 21264 BDD nodes size of Y5 = 1.8092e+13 states, 46137 BDD nodes size of Y6 = 1.85947e+13 states, 86855 BDD nodes size of Y7 = 1.90362e+13 states, 121952 BDD nodes size of Y8 = 1.92708e+13 states, 143174 BDD nodes size of Y9 = 1.94137e+13 states, 143302 BDD nodes size of Y10 = 1.94844e+13 states, 121941 BDD nodes size of Y11 = 1.95154e+13 states, 110024 BDD nodes size of Y12 = 1.95247e+13 states, 102682 BDD nodes size of Y13 = 1.95286e+13 states, 93862 BDD nodes size of Y14 = 1.95302e+13 states, 85923 BDD nodes size of Y15 = 1.95308e+13 states, 80453 BDD nodes size of Y16 = 1.95309e+13 states, 77964 BDD nodes size of Y17 = 1.95309e+13 states, 77456 BDD nodes -- specification AG master3.state != error is true evaluating specification AG slave.state != error eu: computing fixed point approximations for AG slave.state != error ... size of Y1 = 5.66936e+12 states, 4426 BDD nodes size of Y2 = 9.34585e+12 states, 14576 BDD nodes size of Y3 = 1.39501e+13 states, 20292 BDD nodes size of Y4 = 1.44952e+13 states, 21973 BDD nodes size of Y5 = 1.452e+13 states, 21937 BDD nodes -- specification AG slave.state != error is true evaluating specification EF (arbiter.master1_state = mask & arbiter.master2_state = mask) eu: computing fixed point approximations for EF (arbiter.master1_state = mask & arbiter.master2_state = mask) ... size of Y1 = 1.41734e+12 states, 8822 BDD nodes size of Y2 = 1.65249e+12 states, 16184 BDD nodes size of Y3 = 1.95412e+12 states, 23434 BDD nodes size of Y4 = 2.24666e+12 states, 36813 BDD nodes size of Y5 = 2.35142e+12 states, 47061 BDD nodes size of Y6 = 2.46542e+12 states, 54534 BDD nodes size of Y7 = 2.64096e+12 states, 66947 BDD nodes size of Y8 = 3.01238e+12 states, 86132 BDD nodes size of Y9 = 3.32697e+12 states, 117046 BDD nodes size of Y10 = 3.62984e+12 states, 133862 BDD nodes size of Y11 = 3.78961e+12 states, 133428 BDD nodes size of Y12 = 3.93024e+12 states, 128441 BDD nodes size of Y13 = 4.08162e+12 states, 124546 BDD nodes size of Y14 = 4.21592e+12 states, 116639 BDD nodes size of Y15 = 4.24346e+12 states, 105657 BDD nodes size of Y16 = 4.26104e+12 states, 100212 BDD nodes size of Y17 = 4.2672e+12 states, 96274 BDD nodes size of Y18 = 4.26983e+12 states, 91051 BDD nodes size of Y19 = 4.27107e+12 states, 89485 BDD nodes size of Y20 = 4.27216e+12 states, 89806 BDD nodes size of Y21 = 4.27345e+12 states, 87473 BDD nodes size of Y22 = 4.27383e+12 states, 85609 BDD nodes size of Y23 = 4.27389e+12 states, 84993 BDD nodes size of Y24 = 4.27394e+12 states, 84662 BDD nodes size of Y25 = 4.27398e+12 states, 84024 BDD nodes size of Y26 = 4.27398e+12 states, 83795 BDD nodes -- specification EF (arbiter.master1_state = mask & arbiter.master2_state = mask) is true evaluating specification EF ((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) eu: computing fixed point approximations for EF ((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) ... size of Y1 = 3.54335e+11 states, 8830 BDD nodes size of Y2 = 4.14129e+11 states, 16912 BDD nodes size of Y3 = 4.90205e+11 states, 22266 BDD nodes size of Y4 = 5.70654e+11 states, 29272 BDD nodes size of Y5 = 6.0435e+11 states, 33081 BDD nodes size of Y6 = 6.5025e+11 states, 39713 BDD nodes size of Y7 = 7.0862e+11 states, 46878 BDD nodes size of Y8 = 8.11921e+11 states, 60202 BDD nodes size of Y9 = 9.33622e+11 states, 84198 BDD nodes size of Y10 = 1.06517e+12 states, 107431 BDD nodes size of Y11 = 1.19375e+12 states, 120465 BDD nodes size of Y12 = 1.31547e+12 states, 127900 BDD nodes size of Y13 = 1.46961e+12 states, 142257 BDD nodes size of Y14 = 1.62569e+12 states, 136385 BDD nodes size of Y15 = 1.67363e+12 states, 133355 BDD nodes size of Y16 = 1.70904e+12 states, 128292 BDD nodes size of Y17 = 1.75393e+12 states, 127682 BDD nodes size of Y18 = 1.77245e+12 states, 119875 BDD nodes size of Y19 = 1.77795e+12 states, 118428 BDD nodes size of Y20 = 1.78287e+12 states, 118487 BDD nodes size of Y21 = 1.78677e+12 states, 115154 BDD nodes size of Y22 = 1.78794e+12 states, 110366 BDD nodes size of Y23 = 1.78812e+12 states, 108621 BDD nodes size of Y24 = 1.78828e+12 states, 107829 BDD nodes size of Y25 = 1.78837e+12 states, 107052 BDD nodes size of Y26 = 1.7884e+12 states, 106573 BDD nodes -- specification EF ((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) is true evaluating specification AG (((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) -> AF ((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16842 BDD nodes size of Y2 = 5.90296e+20 x, 18985 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 8049 BDD nodes size of res1 = 3.25243e+11 x, 18975 BDD nodes size of Y0 = 1.24554e+11 x, 8048 BDD nodes size of Y1 = 2.08205e+11 x, 18230 BDD nodes size of Y2 = 2.29311e+11 x, 17856 BDD nodes size of Y0 = 2.00689e+11 x, 18967 BDD nodes size of Y1 = 2.60819e+11 x, 19845 BDD nodes size of res2 = 1.64886e+11 x, 11754 BDD nodes size of Y0 = 6.01295e+10 x, 2832 BDD nodes size of Y1 = 1.43781e+11 x, 12128 BDD nodes size of Y2 = 1.64886e+11 x, 11754 BDD nodes size of Y0 = 1.04757e+11 x, 11746 BDD nodes size of Y1 = 1.64886e+11 x, 11754 BDD nodes eu: computing fixed point approximations for AG (((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) -> AF ((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) ... size of Y1 = 1.64886e+11 states, 11754 BDD nodes size of Y2 = 2.19849e+11 states, 11739 BDD nodes size of Y3 = 2.76906e+11 states, 14838 BDD nodes size of Y4 = 3.37915e+11 states, 19717 BDD nodes size of Y5 = 3.63912e+11 states, 22032 BDD nodes size of Y6 = 4.01293e+11 states, 27284 BDD nodes size of Y7 = 4.47501e+11 states, 32280 BDD nodes size of Y8 = 5.1235e+11 states, 40703 BDD nodes size of Y9 = 5.75332e+11 states, 52180 BDD nodes size of Y10 = 6.43027e+11 states, 62510 BDD nodes size of Y11 = 7.07749e+11 states, 69255 BDD nodes size of Y12 = 7.50462e+11 states, 74722 BDD nodes size of Y13 = 7.86933e+11 states, 76628 BDD nodes size of Y14 = 8.16854e+11 states, 72811 BDD nodes size of Y15 = 8.23388e+11 states, 68161 BDD nodes size of Y16 = 8.26305e+11 states, 67498 BDD nodes size of Y17 = 8.27233e+11 states, 69091 BDD nodes size of Y18 = 8.28607e+11 states, 68395 BDD nodes size of Y19 = 8.31195e+11 states, 68156 BDD nodes size of Y20 = 8.34443e+11 states, 69409 BDD nodes size of Y21 = 8.38464e+11 states, 66171 BDD nodes size of Y22 = 8.39669e+11 states, 65353 BDD nodes size of Y23 = 8.39859e+11 states, 64665 BDD nodes size of Y24 = 8.40027e+11 states, 64023 BDD nodes size of Y25 = 8.40133e+11 states, 61762 BDD nodes size of Y26 = 8.40154e+11 states, 60952 BDD nodes -- specification AG (((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) -> AF ((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) is true ###################################################################### Runtime Statistics ------------------ Machine name: node-xeon-9 User time 835.180 seconds System time 0.970 seconds Average resident text size = 0K Average resident data+stack size = 0K Maximum resident size = 0K Virtual text size = 132044K Virtual data size = 45541K data size initialized = 234K data size uninitialized = 362K data size sbrk = 44945K Virtual memory limit = 4194304K (4194304K) Major page faults = 421 Minor page faults = 63109 Swaps = 0 Input blocks = 0 Output blocks = 0 Context switch (voluntary) = 0 Context switch (involuntary) = 0 ###################################################################### BDD statistics -------------------- BDD nodes allocated: 614015 -------------------- BDD nodes representing init set of states: 44 BDD nodes representing state constraints: 8806 BDD nodes representing input constraints: 1 Forward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 2181 cluster 3 : 1927 cluster 4 : 4667 Backward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 2181 cluster 3 : 1927 cluster 4 : 4667