*** 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_2Masters_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 = 1.80144e+16 x, 1 BDD nodes size of Y0 = 4.5036e+15 x, 3 BDD nodes size of Y1 = 4.50361e+15 x, 3846 BDD nodes size of Y2 = 4.50361e+15 x, 2052 BDD nodes size of Y0 = 9.0072e+15 x, 2 BDD nodes size of Y1 = 9.00721e+15 x, 1817 BDD nodes size of res1 = 1.75154e+10 x, 2042 BDD nodes size of Y0 = 6.0398e+09 x, 1816 BDD nodes size of Y1 = 1.47975e+10 x, 3836 BDD nodes size of Y2 = 1.75154e+10 x, 2042 BDD nodes size of Y0 = 1.14756e+10 x, 2034 BDD nodes size of Y1 = 1.75154e+10 x, 2042 BDD nodes done eu: computing fixed point approximations for AG master1.state != error ... size of Y1 = 2.18943e+09 states, 988 BDD nodes size of Y2 = 1.20523e+10 states, 2597 BDD nodes size of Y3 = 1.38422e+10 states, 3009 BDD nodes size of Y4 = 1.40554e+10 states, 4272 BDD nodes size of Y5 = 1.42826e+10 states, 8063 BDD nodes size of Y6 = 1.46233e+10 states, 11059 BDD nodes size of Y7 = 1.49764e+10 states, 14064 BDD nodes size of Y8 = 1.5205e+10 states, 16898 BDD nodes size of Y9 = 1.5333e+10 states, 16973 BDD nodes size of Y10 = 1.53816e+10 states, 14251 BDD nodes size of Y11 = 1.54012e+10 states, 12913 BDD nodes size of Y12 = 1.54056e+10 states, 12317 BDD nodes size of Y13 = 1.54066e+10 states, 11913 BDD nodes size of Y14 = 1.54068e+10 states, 11690 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.18943e+09 states, 772 BDD nodes size of Y2 = 9.6469e+09 states, 3415 BDD nodes size of Y3 = 1.11296e+10 states, 3448 BDD nodes size of Y4 = 1.20117e+10 states, 4518 BDD nodes size of Y5 = 1.25637e+10 states, 7819 BDD nodes size of Y6 = 1.30697e+10 states, 12115 BDD nodes size of Y7 = 1.3489e+10 states, 16006 BDD nodes size of Y8 = 1.3671e+10 states, 19050 BDD nodes size of Y9 = 1.37459e+10 states, 19265 BDD nodes size of Y10 = 1.37761e+10 states, 16093 BDD nodes size of Y11 = 1.37921e+10 states, 14302 BDD nodes size of Y12 = 1.37943e+10 states, 13424 BDD nodes size of Y13 = 1.37945e+10 states, 13006 BDD nodes size of Y14 = 1.37945e+10 states, 12788 BDD nodes -- specification AG master2.state != error is true evaluating specification AG slave.state != error eu: computing fixed point approximations for AG slave.state != error ... size of Y1 = 4.37885e+09 states, 1036 BDD nodes size of Y2 = 7.19743e+09 states, 3630 BDD nodes size of Y3 = 1.07332e+10 states, 5208 BDD nodes size of Y4 = 1.11964e+10 states, 5689 BDD nodes size of Y5 = 1.12206e+10 states, 5677 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.09471e+09 states, 2054 BDD nodes size of Y2 = 1.29761e+09 states, 4323 BDD nodes size of Y3 = 1.54878e+09 states, 5917 BDD nodes size of Y4 = 1.80863e+09 states, 7838 BDD nodes size of Y5 = 1.91802e+09 states, 9393 BDD nodes size of Y6 = 2.0242e+09 states, 10547 BDD nodes size of Y7 = 2.15187e+09 states, 12082 BDD nodes size of Y8 = 2.40495e+09 states, 13715 BDD nodes size of Y9 = 2.65896e+09 states, 15668 BDD nodes size of Y10 = 2.97967e+09 states, 16913 BDD nodes size of Y11 = 3.22622e+09 states, 17275 BDD nodes size of Y12 = 3.37562e+09 states, 17538 BDD nodes size of Y13 = 3.52386e+09 states, 18648 BDD nodes size of Y14 = 3.67729e+09 states, 17115 BDD nodes size of Y15 = 3.70154e+09 states, 15713 BDD nodes size of Y16 = 3.71456e+09 states, 15146 BDD nodes -- specification EF (arbiter.master1_state = mask & arbiter.master2_state = mask) is true evaluating specification AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) size of res0 = 1.80144e+16 x, 1 BDD nodes size of Y0 = 4.5036e+15 x, 3 BDD nodes size of Y1 = 4.5036e+15 x, 3858 BDD nodes size of Y2 = 4.5036e+15 x, 4533 BDD nodes size of Y0 = 9.0072e+15 x, 2 BDD nodes size of Y1 = 9.0072e+15 x, 1829 BDD nodes size of res1 = 9.90118e+08 x, 4523 BDD nodes size of Y0 = 3.77487e+08 x, 1828 BDD nodes size of Y1 = 5.93756e+08 x, 4803 BDD nodes size of Y2 = 6.42253e+08 x, 4632 BDD nodes size of Y0 = 6.12631e+08 x, 4515 BDD nodes size of Y1 = 7.63625e+08 x, 4785 BDD nodes size of res2 = 4.1576e+08 x, 3385 BDD nodes size of Y0 = 1.50995e+08 x, 859 BDD nodes size of Y1 = 3.67264e+08 x, 3556 BDD nodes size of Y2 = 4.1576e+08 x, 3385 BDD nodes size of Y0 = 2.64765e+08 x, 3377 BDD nodes size of Y1 = 4.1576e+08 x, 3385 BDD nodes eu: computing fixed point approximations for AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) ... size of Y1 = 4.1576e+08 states, 3385 BDD nodes size of Y2 = 5.84057e+08 states, 3376 BDD nodes size of Y3 = 7.03463e+08 states, 4318 BDD nodes size of Y4 = 8.34851e+08 states, 5652 BDD nodes size of Y5 = 8.95787e+08 states, 6572 BDD nodes size of Y6 = 9.59259e+08 states, 7385 BDD nodes size of Y7 = 1.03101e+09 states, 8305 BDD nodes size of Y8 = 1.10521e+09 states, 9006 BDD nodes size of Y9 = 1.11879e+09 states, 8839 BDD nodes size of Y10 = 1.13041e+09 states, 7904 BDD nodes size of Y11 = 1.13326e+09 states, 7696 BDD nodes -- specification AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) is true ###################################################################### Runtime Statistics ------------------ Machine name: node-xeon-5 User time 8.160 seconds System time 0.100 seconds Average resident text size = 0K Average resident data+stack size = 0K Maximum resident size = 0K Virtual text size = 132044K Virtual data size = 10985K data size initialized = 234K data size uninitialized = 362K data size sbrk = 10389K Virtual memory limit = 4194304K (4194304K) Major page faults = 408 Minor page faults = 4483 Swaps = 0 Input blocks = 0 Output blocks = 0 Context switch (voluntary) = 0 Context switch (involuntary) = 0 ###################################################################### BDD statistics -------------------- BDD nodes allocated: 268654 -------------------- BDD nodes representing init set of states: 33 BDD nodes representing state constraints: 2042 BDD nodes representing input constraints: 1 Forward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 10942 cluster 3 : 1238 Backward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 10942 cluster 3 : 1238