*** 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_Deadlock.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, 3636 BDD nodes size of Y2 = 4.50361e+15 x, 1842 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.81194e+10 x, 1816 BDD nodes size of Y0 = 6.0398e+09 x, 1816 BDD nodes size of Y1 = 1.50995e+10 x, 3610 BDD nodes size of Y2 = 1.81194e+10 x, 1816 BDD nodes size of Y0 = 1.20796e+10 x, 1808 BDD nodes size of Y1 = 1.81194e+10 x, 1816 BDD nodes done eu: computing fixed point approximations for AG master1.state != error ... size of Y1 = 2.26492e+09 states, 896 BDD nodes size of Y2 = 1.24707e+10 states, 2659 BDD nodes size of Y3 = 1.42661e+10 states, 3171 BDD nodes size of Y4 = 1.44905e+10 states, 4543 BDD nodes size of Y5 = 1.4727e+10 states, 8524 BDD nodes size of Y6 = 1.508e+10 states, 11535 BDD nodes size of Y7 = 1.54502e+10 states, 14464 BDD nodes size of Y8 = 1.57028e+10 states, 17284 BDD nodes size of Y9 = 1.5848e+10 states, 17231 BDD nodes size of Y10 = 1.59017e+10 states, 14571 BDD nodes size of Y11 = 1.59237e+10 states, 13313 BDD nodes size of Y12 = 1.59289e+10 states, 12769 BDD nodes size of Y13 = 1.59301e+10 states, 12374 BDD nodes size of Y14 = 1.59304e+10 states, 12159 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.26492e+09 states, 666 BDD nodes size of Y2 = 9.82306e+09 states, 3621 BDD nodes size of Y3 = 1.13498e+10 states, 3687 BDD nodes size of Y4 = 1.23216e+10 states, 4750 BDD nodes size of Y5 = 1.29402e+10 states, 8123 BDD nodes size of Y6 = 1.34794e+10 states, 12319 BDD nodes size of Y7 = 1.39291e+10 states, 16330 BDD nodes size of Y8 = 1.41394e+10 states, 19299 BDD nodes size of Y9 = 1.42231e+10 states, 19373 BDD nodes size of Y10 = 1.42534e+10 states, 16276 BDD nodes size of Y11 = 1.4271e+10 states, 14517 BDD nodes size of Y12 = 1.42737e+10 states, 13654 BDD nodes size of Y13 = 1.42739e+10 states, 13245 BDD nodes size of Y14 = 1.4274e+10 states, 13035 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.52985e+09 states, 923 BDD nodes size of Y2 = 7.46167e+09 states, 4048 BDD nodes size of Y3 = 1.10824e+10 states, 5983 BDD nodes size of Y4 = 1.16376e+10 states, 6630 BDD nodes size of Y5 = 1.16689e+10 states, 6618 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.13246e+09 states, 1828 BDD nodes size of Y2 = 1.35306e+09 states, 4740 BDD nodes size of Y3 = 1.60422e+09 states, 6334 BDD nodes size of Y4 = 1.87568e+09 states, 7835 BDD nodes size of Y5 = 1.99835e+09 states, 9378 BDD nodes size of Y6 = 2.13179e+09 states, 10826 BDD nodes size of Y7 = 2.2607e+09 states, 12361 BDD nodes size of Y8 = 2.51502e+09 states, 13988 BDD nodes size of Y9 = 2.77263e+09 states, 15950 BDD nodes size of Y10 = 3.11116e+09 states, 17165 BDD nodes size of Y11 = 3.38598e+09 states, 17566 BDD nodes size of Y12 = 3.55624e+09 states, 17920 BDD nodes size of Y13 = 3.70957e+09 states, 19017 BDD nodes size of Y14 = 3.86712e+09 states, 17499 BDD nodes size of Y15 = 3.89377e+09 states, 16129 BDD nodes size of Y16 = 3.90725e+09 states, 15578 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, 3648 BDD nodes size of Y2 = 4.5036e+15 x, 4950 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 = 1.00958e+09 x, 4940 BDD nodes size of Y0 = 3.77487e+08 x, 1828 BDD nodes size of Y1 = 5.94346e+08 x, 5220 BDD nodes size of Y2 = 6.43432e+08 x, 5049 BDD nodes size of Y0 = 6.32095e+08 x, 4932 BDD nodes size of Y1 = 7.8309e+08 x, 5202 BDD nodes size of res2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 1.50995e+08 x, 859 BDD nodes size of Y1 = 3.67854e+08 x, 3973 BDD nodes size of Y2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 2.65945e+08 x, 3794 BDD nodes size of Y1 = 4.1694e+08 x, 3802 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.1694e+08 states, 3802 BDD nodes size of Y2 = 6.02931e+08 states, 3793 BDD nodes size of Y3 = 8.35584e+08 states, 5736 BDD nodes size of Y4 = 9.79358e+08 states, 6872 BDD nodes size of Y5 = 1.05445e+09 states, 7798 BDD nodes size of Y6 = 1.16049e+09 states, 9113 BDD nodes size of Y7 = 1.26311e+09 states, 10970 BDD nodes size of Y8 = 1.36573e+09 states, 12974 BDD nodes size of Y9 = 1.43498e+09 states, 14235 BDD nodes size of Y10 = 1.575e+09 states, 14271 BDD nodes size of Y11 = 1.89939e+09 states, 14854 BDD nodes size of Y12 = 2.2645e+09 states, 16178 BDD nodes size of Y13 = 2.62684e+09 states, 17582 BDD nodes size of Y14 = 2.91081e+09 states, 17909 BDD nodes size of Y15 = 3.08287e+09 states, 18287 BDD nodes size of Y16 = 3.23923e+09 states, 19356 BDD nodes size of Y17 = 3.39931e+09 states, 17743 BDD nodes size of Y18 = 3.4268e+09 states, 16354 BDD nodes size of Y19 = 3.44042e+09 states, 15813 BDD nodes -- specification AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) is false 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, 3648 BDD nodes size of Y2 = 4.5036e+15 x, 4950 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 = 1.00958e+09 x, 4940 BDD nodes size of Y0 = 3.77487e+08 x, 1828 BDD nodes size of Y1 = 5.94346e+08 x, 5220 BDD nodes size of Y2 = 6.43432e+08 x, 5049 BDD nodes size of Y0 = 6.32095e+08 x, 4932 BDD nodes size of Y1 = 7.8309e+08 x, 5202 BDD nodes size of res2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 1.50995e+08 x, 859 BDD nodes size of Y1 = 3.67854e+08 x, 3973 BDD nodes size of Y2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 2.65945e+08 x, 3794 BDD nodes size of Y1 = 4.1694e+08 x, 3802 BDD nodes searching (counter)example for E [ 1 U (!((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask))) ] eu_explain: iteration 0: states = 1, BDD nodes = 55 eu_explain: iteration 1: states = 2, BDD nodes = 54 eu_explain: iteration 2: states = 8, BDD nodes = 86 eu_explain: iteration 3: states = 44, BDD nodes = 216 eu_explain: iteration 4: states = 104, BDD nodes = 319 eu_explain: iteration 5: states = 304, BDD nodes = 482 eu_explain: iteration 6: states = 504, BDD nodes = 634 eu_explain: iteration 7: states = 632, BDD nodes = 1105 eu_explain: iteration 8: states = 821, BDD nodes = 1610 eu_explain: iteration 9: states = 939, BDD nodes = 1767 eu_explain: iteration 10: states = 1215, BDD nodes = 1891 eu_explain: iteration 11: states = 1975, BDD nodes = 2023 eu_explain: iteration 12: states = 2735, BDD nodes = 2178 eu_explain: iteration 13: states = 3219, BDD nodes = 2490 eu_explain: iteration 14: states = 4023, BDD nodes = 2956 eu_explain: iteration 15: states = 4431, BDD nodes = 3017 eu_explain: iteration 16: states = 4975, BDD nodes = 3257 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, 3648 BDD nodes size of Y2 = 4.5036e+15 x, 4950 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 = 1.00958e+09 x, 4940 BDD nodes size of Y0 = 3.77487e+08 x, 1828 BDD nodes size of Y1 = 5.94346e+08 x, 5220 BDD nodes size of Y2 = 6.43432e+08 x, 5049 BDD nodes size of Y0 = 6.32095e+08 x, 4932 BDD nodes size of Y1 = 7.8309e+08 x, 5202 BDD nodes size of res2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 1.50995e+08 x, 859 BDD nodes size of Y1 = 3.67854e+08 x, 3973 BDD nodes size of Y2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 2.65945e+08 x, 3794 BDD nodes size of Y1 = 4.1694e+08 x, 3802 BDD nodes 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, 3648 BDD nodes size of Y2 = 4.5036e+15 x, 4950 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 = 1.00958e+09 x, 4940 BDD nodes size of Y0 = 3.77487e+08 x, 1828 BDD nodes size of Y1 = 5.94346e+08 x, 5220 BDD nodes size of Y2 = 6.43432e+08 x, 5049 BDD nodes size of Y0 = 6.32095e+08 x, 4932 BDD nodes size of Y1 = 7.8309e+08 x, 5202 BDD nodes size of res2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 1.50995e+08 x, 859 BDD nodes size of Y1 = 3.67854e+08 x, 3973 BDD nodes size of Y2 = 4.1694e+08 x, 3802 BDD nodes size of Y0 = 2.65945e+08 x, 3794 BDD nodes size of Y1 = 4.1694e+08 x, 3802 BDD nodes searching (counter)example for EG (!(arbiter.master1_state != mask | arbiter.master2_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 55 eu_explain: iteration 1: states = 5, BDD nodes = 117 searching (counter)example for EG (!(arbiter.master1_state != mask | arbiter.master2_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 55 eu_explain: iteration 1: states = 3, BDD nodes = 101 searching (counter)example for EG (!(arbiter.master1_state != mask | arbiter.master2_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 55 eu_explain: iteration 1: states = 2, BDD nodes = 54 searching (counter)example for EG (!(arbiter.master1_state != mask | arbiter.master2_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 55 searching (counter)example for EG (!(arbiter.master1_state != mask | arbiter.master2_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 55 eu_explain: iteration 1: states = 2, BDD nodes = 54 searching (counter)example for EG (!(arbiter.master1_state != mask | arbiter.master2_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 55 -- as demonstrated by the following execution sequence Trace Description: CTL Counterexample Trace Type: Counterexample -> State: 1.1 <- HADDR = 0 HTRANS = IDLE HWDATA = 0 HRDATA = 0 HREADY = 0 HRESP = OK BUSREQ1 = 0 BUSREQ2 = 0 HGRANT1 = 0 HGRANT2 = 0 HMASTER = default HSPLIT = 0 master1.state = idle master1.prev_state = idle master1.HADDR = 0 master1.HTRANS = IDLE master1.HWDATA = 0 master2.state = idle master2.prev_state = idle master2.HADDR = 0 master2.HTRANS = IDLE master2.HWDATA = 0 slave.state = idle slave.prev_state = idle slave.MASK_MASTER1 = 0 slave.MASK_MASTER2 = 0 slave.extended = 0 arbiter.master1_state = idle arbiter.master2_state = idle arbiter.master1_prev_state = idle arbiter.master2_prev_state = idle arbiter.lasterror = 0 arbiter.preferred = default -> State: 1.2 <- HREADY = 1 -> State: 1.3 <- BUSREQ1 = 1 master1.state = busreq -> State: 1.4 <- HGRANT1 = 1 HMASTER = master1 master1.prev_state = busreq arbiter.preferred = master1 -> State: 1.5 <- HADDR = 1 HTRANS = NONSEQ BUSREQ1 = 0 master1.state = haddr master1.HADDR = 1 master1.HTRANS = NONSEQ arbiter.master1_state = grant -> State: 1.6 <- HADDR = 0 HTRANS = SEQ HRDATA = 1 master1.state = read master1.prev_state = haddr master1.HADDR = 0 master1.HTRANS = SEQ slave.state = write arbiter.master1_state = transmit arbiter.master1_prev_state = grant -> State: 1.7 <- HWDATA = 1 HRDATA = 0 HRESP = SPLIT master1.state = write master1.prev_state = read master1.HWDATA = 1 slave.state = read slave.prev_state = write arbiter.master1_prev_state = transmit -> State: 1.8 <- HTRANS = IDLE HWDATA = 0 BUSREQ2 = 1 HGRANT1 = 0 HMASTER = default master1.state = idle master1.prev_state = write master1.HTRANS = IDLE master1.HWDATA = 0 master2.state = busreq slave.state = idle slave.prev_state = read slave.MASK_MASTER1 = 1 slave.extended = 1 arbiter.master1_state = mask arbiter.lasterror = 1 arbiter.preferred = default -> State: 1.9 <- HRESP = OK master1.prev_state = idle master2.prev_state = busreq slave.prev_state = idle slave.extended = 0 arbiter.master1_prev_state = mask -> State: 1.10 <- BUSREQ1 = 1 HGRANT2 = 1 HMASTER = master2 master1.state = busreq arbiter.lasterror = 0 arbiter.preferred = master2 -> State: 1.11 <- HADDR = 1 HTRANS = NONSEQ BUSREQ2 = 0 master1.prev_state = busreq master2.state = haddr master2.HADDR = 1 master2.HTRANS = NONSEQ arbiter.master2_state = grant -> State: 1.12 <- HADDR = 0 HTRANS = SEQ HRDATA = 1 master2.state = read master2.prev_state = haddr master2.HADDR = 0 master2.HTRANS = SEQ slave.state = write arbiter.master2_state = transmit arbiter.master2_prev_state = grant -> State: 1.13 <- HWDATA = 1 HRDATA = 0 HRESP = RETRY HSPLIT = master1 master2.state = write master2.prev_state = read master2.HWDATA = 1 slave.state = read slave.prev_state = write arbiter.master2_prev_state = transmit -> State: 1.14 <- HWDATA = 0 HRDATA = 1 HSPLIT = 0 master2.state = read master2.prev_state = write master2.HWDATA = 0 slave.state = write slave.prev_state = read slave.MASK_MASTER1 = 0 slave.extended = 1 arbiter.lasterror = 1 -> State: 1.15 <- HWDATA = 1 HRDATA = 0 HRESP = OK master2.state = write master2.prev_state = read master2.HWDATA = 1 slave.state = read slave.prev_state = write slave.extended = 0 -> State: 1.16 <- HTRANS = IDLE HWDATA = 0 HRESP = SPLIT master2.state = idle master2.prev_state = write master2.HTRANS = IDLE master2.HWDATA = 0 slave.state = idle slave.prev_state = read arbiter.lasterror = 0 -> State: 1.17 <- HGRANT2 = 0 HMASTER = default master2.prev_state = idle slave.prev_state = idle slave.MASK_MASTER2 = 1 slave.extended = 1 arbiter.master2_state = mask arbiter.lasterror = 1 arbiter.preferred = default -> State: 1.18 <- HREADY = 0 HRESP = OK BUSREQ2 = 1 master2.state = busreq slave.extended = 0 arbiter.master2_prev_state = mask -> State: 1.19 <- HREADY = 1 master2.prev_state = busreq arbiter.lasterror = 0 -- Loop starts here -> State: 1.20 <- HREADY = 0 -> State: 1.21 <- HREADY = 1 -> State: 1.22 <- HREADY = 0 ###################################################################### Runtime Statistics ------------------ Machine name: node-xeon-5 User time 9.180 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 = 11361K data size initialized = 234K data size uninitialized = 362K data size sbrk = 10765K Virtual memory limit = 4194304K (4194304K) Major page faults = 415 Minor page faults = 4473 Swaps = 0 Input blocks = 0 Output blocks = 0 Context switch (voluntary) = 0 Context switch (involuntary) = 0 ###################################################################### BDD statistics -------------------- BDD nodes allocated: 316517 -------------------- BDD nodes representing init set of states: 33 BDD nodes representing state constraints: 1816 BDD nodes representing input constraints: 1 Forward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 10876 cluster 3 : 1238 Backward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 10876 cluster 3 : 1238