*** 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_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 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16052 BDD nodes size of Y2 = 5.90296e+20 x, 8050 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.39144e+13 x, 8024 BDD nodes size of Y0 = 7.97146e+12 x, 8024 BDD nodes size of Y1 = 1.99286e+13 x, 16026 BDD nodes size of Y2 = 2.39144e+13 x, 8024 BDD nodes size of Y0 = 1.59429e+13 x, 8016 BDD nodes size of Y1 = 2.39144e+13 x, 8024 BDD nodes done eu: computing fixed point approximations for AG master1.state != error ... size of Y1 = 2.9893e+12 states, 4374 BDD nodes size of Y2 = 1.57024e+13 states, 10845 BDD nodes size of Y3 = 1.80079e+13 states, 12564 BDD nodes size of Y4 = 1.85283e+13 states, 21984 BDD nodes size of Y5 = 1.8964e+13 states, 48831 BDD nodes size of Y6 = 1.95033e+13 states, 74381 BDD nodes size of Y7 = 1.99876e+13 states, 102978 BDD nodes size of Y8 = 2.02689e+13 states, 134956 BDD nodes size of Y9 = 2.04393e+13 states, 128894 BDD nodes size of Y10 = 2.05189e+13 states, 105531 BDD nodes size of Y11 = 2.05551e+13 states, 97489 BDD nodes size of Y12 = 2.05671e+13 states, 91314 BDD nodes size of Y13 = 2.05718e+13 states, 83602 BDD nodes size of Y14 = 2.05737e+13 states, 76700 BDD nodes size of Y15 = 2.05744e+13 states, 72489 BDD nodes size of Y16 = 2.05746e+13 states, 70337 BDD nodes size of Y17 = 2.05746e+13 states, 69947 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.9893e+12 states, 3492 BDD nodes size of Y2 = 1.57024e+13 states, 14810 BDD nodes size of Y3 = 1.80079e+13 states, 14653 BDD nodes size of Y4 = 1.85283e+13 states, 23178 BDD nodes size of Y5 = 1.8964e+13 states, 51783 BDD nodes size of Y6 = 1.95033e+13 states, 83509 BDD nodes size of Y7 = 1.99876e+13 states, 113141 BDD nodes size of Y8 = 2.02689e+13 states, 141504 BDD nodes size of Y9 = 2.04393e+13 states, 134387 BDD nodes size of Y10 = 2.05189e+13 states, 111137 BDD nodes size of Y11 = 2.05551e+13 states, 101987 BDD nodes size of Y12 = 2.05671e+13 states, 94215 BDD nodes size of Y13 = 2.05718e+13 states, 86585 BDD nodes size of Y14 = 2.05737e+13 states, 81025 BDD nodes size of Y15 = 2.05744e+13 states, 76004 BDD nodes size of Y16 = 2.05746e+13 states, 73769 BDD nodes size of Y17 = 2.05746e+13 states, 73316 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.9893e+12 states, 3138 BDD nodes size of Y2 = 1.57024e+13 states, 16367 BDD nodes size of Y3 = 1.80079e+13 states, 15493 BDD nodes size of Y4 = 1.85283e+13 states, 22938 BDD nodes size of Y5 = 1.8964e+13 states, 49540 BDD nodes size of Y6 = 1.95033e+13 states, 91287 BDD nodes size of Y7 = 1.99876e+13 states, 123503 BDD nodes size of Y8 = 2.02689e+13 states, 150793 BDD nodes size of Y9 = 2.04393e+13 states, 146756 BDD nodes size of Y10 = 2.05189e+13 states, 124314 BDD nodes size of Y11 = 2.05551e+13 states, 113034 BDD nodes size of Y12 = 2.05671e+13 states, 104940 BDD nodes size of Y13 = 2.05718e+13 states, 95611 BDD nodes size of Y14 = 2.05737e+13 states, 87627 BDD nodes size of Y15 = 2.05744e+13 states, 82176 BDD nodes size of Y16 = 2.05746e+13 states, 79714 BDD nodes size of Y17 = 2.05746e+13 states, 79209 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.97859e+12 states, 4035 BDD nodes size of Y2 = 9.88701e+12 states, 17890 BDD nodes size of Y3 = 1.46652e+13 states, 25518 BDD nodes size of Y4 = 1.53988e+13 states, 28343 BDD nodes size of Y5 = 1.54381e+13 states, 28307 BDD nodes -- specification AG slave.state != error 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.73662e+11 states, 8048 BDD nodes size of Y2 = 4.42969e+11 states, 20224 BDD nodes size of Y3 = 5.19045e+11 states, 25578 BDD nodes size of Y4 = 6.0596e+11 states, 31552 BDD nodes size of Y5 = 6.47013e+11 states, 36329 BDD nodes size of Y6 = 7.03009e+11 states, 45346 BDD nodes size of Y7 = 7.62104e+11 states, 52980 BDD nodes size of Y8 = 8.65902e+11 states, 66793 BDD nodes size of Y9 = 9.93301e+11 states, 88670 BDD nodes size of Y10 = 1.13797e+12 states, 110553 BDD nodes size of Y11 = 1.28669e+12 states, 123536 BDD nodes size of Y12 = 1.42275e+12 states, 130741 BDD nodes size of Y13 = 1.58173e+12 states, 143991 BDD nodes size of Y14 = 1.75247e+12 states, 138510 BDD nodes size of Y15 = 1.81684e+12 states, 136540 BDD nodes size of Y16 = 1.85544e+12 states, 132167 BDD nodes size of Y17 = 1.90178e+12 states, 131934 BDD nodes size of Y18 = 1.92187e+12 states, 124451 BDD nodes size of Y19 = 1.92815e+12 states, 123165 BDD nodes size of Y20 = 1.93305e+12 states, 123414 BDD nodes size of Y21 = 1.93767e+12 states, 120088 BDD nodes size of Y22 = 1.93961e+12 states, 115664 BDD nodes size of Y23 = 1.93984e+12 states, 114250 BDD nodes size of Y24 = 1.94002e+12 states, 113504 BDD nodes size of Y25 = 1.94016e+12 states, 112726 BDD nodes size of Y26 = 1.94019e+12 states, 112289 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, 16076 BDD nodes size of Y2 = 5.90296e+20 x, 22297 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.34982e+11 x, 22287 BDD nodes size of Y0 = 1.24554e+11 x, 8048 BDD nodes size of Y1 = 2.08281e+11 x, 21542 BDD nodes size of Y2 = 2.29462e+11 x, 21168 BDD nodes size of Y0 = 2.10428e+11 x, 22279 BDD nodes size of Y1 = 2.70558e+11 x, 23157 BDD nodes size of res2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 6.01295e+10 x, 2832 BDD nodes size of Y1 = 1.43856e+11 x, 15440 BDD nodes size of Y2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 1.04908e+11 x, 15058 BDD nodes size of Y1 = 1.65037e+11 x, 15066 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.65037e+11 states, 15066 BDD nodes size of Y2 = 2.29512e+11 states, 15051 BDD nodes size of Y3 = 3.18782e+11 states, 23430 BDD nodes size of Y4 = 3.86359e+11 states, 28023 BDD nodes size of Y5 = 4.1983e+11 states, 31378 BDD nodes size of Y6 = 4.69517e+11 states, 39599 BDD nodes size of Y7 = 5.20801e+11 states, 47789 BDD nodes size of Y8 = 5.89931e+11 states, 60895 BDD nodes size of Y9 = 6.67707e+11 states, 83737 BDD nodes size of Y10 = 7.68963e+11 states, 103821 BDD nodes size of Y11 = 9.12594e+11 states, 124840 BDD nodes size of Y12 = 1.04904e+12 states, 139782 BDD nodes size of Y13 = 1.16293e+12 states, 150108 BDD nodes size of Y14 = 1.26439e+12 states, 146320 BDD nodes size of Y15 = 1.35651e+12 states, 141115 BDD nodes size of Y16 = 1.47779e+12 states, 147728 BDD nodes size of Y17 = 1.61832e+12 states, 141162 BDD nodes size of Y18 = 1.67499e+12 states, 138522 BDD nodes size of Y19 = 1.71305e+12 states, 134883 BDD nodes size of Y20 = 1.76207e+12 states, 132702 BDD nodes size of Y21 = 1.78445e+12 states, 123145 BDD nodes size of Y22 = 1.79011e+12 states, 116499 BDD nodes size of Y23 = 1.79175e+12 states, 114545 BDD nodes size of Y24 = 1.79196e+12 states, 113861 BDD nodes size of Y25 = 1.7921e+12 states, 113120 BDD nodes size of Y26 = 1.79214e+12 states, 112731 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 false 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, 16076 BDD nodes size of Y2 = 5.90296e+20 x, 22297 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.34982e+11 x, 22287 BDD nodes size of Y0 = 1.24554e+11 x, 8048 BDD nodes size of Y1 = 2.08281e+11 x, 21542 BDD nodes size of Y2 = 2.29462e+11 x, 21168 BDD nodes size of Y0 = 2.10428e+11 x, 22279 BDD nodes size of Y1 = 2.70558e+11 x, 23157 BDD nodes size of res2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 6.01295e+10 x, 2832 BDD nodes size of Y1 = 1.43856e+11 x, 15440 BDD nodes size of Y2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 1.04908e+11 x, 15058 BDD nodes size of Y1 = 1.65037e+11 x, 15066 BDD nodes searching (counter)example for E [ 1 U (!(((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))) ] eu_explain: iteration 0: states = 1, BDD nodes = 72 eu_explain: iteration 1: states = 2, BDD nodes = 71 eu_explain: iteration 2: states = 16, BDD nodes = 171 eu_explain: iteration 3: states = 84, BDD nodes = 573 eu_explain: iteration 4: states = 192, BDD nodes = 879 eu_explain: iteration 5: states = 504, BDD nodes = 1369 eu_explain: iteration 6: states = 816, BDD nodes = 1838 eu_explain: iteration 7: states = 1044, BDD nodes = 3451 eu_explain: iteration 8: states = 1677, BDD nodes = 6186 eu_explain: iteration 9: states = 3327, BDD nodes = 9231 eu_explain: iteration 10: states = 7683, BDD nodes = 11396 eu_explain: iteration 11: states = 12675, BDD nodes = 11867 eu_explain: iteration 12: states = 16581, BDD nodes = 14677 eu_explain: iteration 13: states = 20853, BDD nodes = 17529 eu_explain: iteration 14: states = 26073, BDD nodes = 18746 eu_explain: iteration 15: states = 31761, BDD nodes = 20802 eu_explain: iteration 16: states = 38871, BDD nodes = 22326 eu_explain: iteration 17: states = 45558, BDD nodes = 24725 eu_explain: iteration 18: states = 53448, BDD nodes = 27280 eu_explain: iteration 19: states = 61119, BDD nodes = 27972 eu_explain: iteration 20: states = 66660, BDD nodes = 26375 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, 16076 BDD nodes size of Y2 = 5.90296e+20 x, 22297 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.34982e+11 x, 22287 BDD nodes size of Y0 = 1.24554e+11 x, 8048 BDD nodes size of Y1 = 2.08281e+11 x, 21542 BDD nodes size of Y2 = 2.29462e+11 x, 21168 BDD nodes size of Y0 = 2.10428e+11 x, 22279 BDD nodes size of Y1 = 2.70558e+11 x, 23157 BDD nodes size of res2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 6.01295e+10 x, 2832 BDD nodes size of Y1 = 1.43856e+11 x, 15440 BDD nodes size of Y2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 1.04908e+11 x, 15058 BDD nodes size of Y1 = 1.65037e+11 x, 15066 BDD nodes 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, 16076 BDD nodes size of Y2 = 5.90296e+20 x, 22297 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.34982e+11 x, 22287 BDD nodes size of Y0 = 1.24554e+11 x, 8048 BDD nodes size of Y1 = 2.08281e+11 x, 21542 BDD nodes size of Y2 = 2.29462e+11 x, 21168 BDD nodes size of Y0 = 2.10428e+11 x, 22279 BDD nodes size of Y1 = 2.70558e+11 x, 23157 BDD nodes size of res2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 6.01295e+10 x, 2832 BDD nodes size of Y1 = 1.43856e+11 x, 15440 BDD nodes size of Y2 = 1.65037e+11 x, 15066 BDD nodes size of Y0 = 1.04908e+11 x, 15058 BDD nodes size of Y1 = 1.65037e+11 x, 15066 BDD nodes searching (counter)example for EG (!((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 72 eu_explain: iteration 1: states = 5, BDD nodes = 162 searching (counter)example for EG (!((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 72 eu_explain: iteration 1: states = 3, BDD nodes = 135 searching (counter)example for EG (!((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 72 eu_explain: iteration 1: states = 2, BDD nodes = 71 searching (counter)example for EG (!((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 72 searching (counter)example for EG (!((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 72 eu_explain: iteration 1: states = 2, BDD nodes = 71 searching (counter)example for EG (!((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) eu_explain: iteration 0: states = 1, BDD nodes = 72 -- 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 BUSREQ3 = 0 HGRANT1 = 0 HGRANT2 = 0 HGRANT3 = 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 master3.state = idle master3.prev_state = idle master3.HADDR = 0 master3.HTRANS = IDLE master3.HWDATA = 0 slave.state = idle slave.prev_state = idle slave.MASK_MASTER1 = 0 slave.MASK_MASTER2 = 0 slave.MASK_MASTER3 = 0 slave.extended = 0 arbiter.master1_state = idle arbiter.master2_state = idle arbiter.master3_state = idle arbiter.master1_prev_state = idle arbiter.master2_prev_state = idle arbiter.master3_prev_state = idle arbiter.lasterror = 0 arbiter.preferred = default -> State: 1.2 <- HREADY = 1 -> State: 1.3 <- BUSREQ1 = 1 BUSREQ2 = 1 BUSREQ3 = 1 master1.state = busreq master2.state = busreq master3.state = busreq -> State: 1.4 <- HGRANT2 = 1 HMASTER = master2 master1.prev_state = busreq master2.prev_state = busreq master3.prev_state = busreq arbiter.preferred = master2 -> State: 1.5 <- HADDR = 1 HTRANS = NONSEQ BUSREQ2 = 0 master2.state = haddr master2.HADDR = 1 master2.HTRANS = NONSEQ arbiter.master2_state = grant -> State: 1.6 <- 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.7 <- HWDATA = 1 HRDATA = 0 HRESP = SPLIT master2.state = write master2.prev_state = read master2.HWDATA = 1 slave.state = read slave.prev_state = write arbiter.master2_prev_state = transmit -> State: 1.8 <- HTRANS = IDLE HWDATA = 0 HGRANT2 = 0 HGRANT3 = 1 HMASTER = master3 master2.state = idle master2.prev_state = write master2.HTRANS = IDLE master2.HWDATA = 0 slave.state = idle slave.prev_state = read slave.MASK_MASTER2 = 1 slave.extended = 1 arbiter.master2_state = mask arbiter.lasterror = 1 arbiter.preferred = master3 -> State: 1.9 <- HRESP = OK BUSREQ2 = 1 BUSREQ3 = 0 HGRANT1 = 1 HGRANT3 = 0 HMASTER = master1 master2.state = busreq master2.prev_state = idle master3.state = idle slave.prev_state = idle slave.extended = 0 arbiter.master2_prev_state = mask arbiter.preferred = master1 -> State: 1.10 <- HADDR = 1 HTRANS = NONSEQ BUSREQ1 = 0 master1.state = haddr master1.HADDR = 1 master1.HTRANS = NONSEQ master2.prev_state = busreq master3.prev_state = idle arbiter.master1_state = grant arbiter.lasterror = 0 -> State: 1.11 <- 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.12 <- 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.13 <- HTRANS = IDLE HWDATA = 0 BUSREQ3 = 1 master1.state = idle master1.prev_state = write master1.HTRANS = IDLE master1.HWDATA = 0 master3.state = busreq slave.state = idle slave.prev_state = read slave.MASK_MASTER1 = 1 slave.extended = 1 arbiter.master1_state = mask arbiter.lasterror = 1 -> State: 1.14 <- HRESP = OK HGRANT1 = 0 HGRANT3 = 1 HMASTER = master3 master1.prev_state = idle master3.prev_state = busreq slave.prev_state = idle slave.extended = 0 arbiter.master1_prev_state = mask arbiter.preferred = master3 -> State: 1.15 <- HADDR = 1 HTRANS = NONSEQ BUSREQ3 = 0 master3.state = haddr master3.HADDR = 1 master3.HTRANS = NONSEQ arbiter.master3_state = grant arbiter.lasterror = 0 -> State: 1.16 <- HADDR = 0 HTRANS = SEQ HRDATA = 1 master3.state = read master3.prev_state = haddr master3.HADDR = 0 master3.HTRANS = SEQ slave.state = write arbiter.master3_state = transmit arbiter.master3_prev_state = grant -> State: 1.17 <- HWDATA = 1 HRDATA = 0 HRESP = RETRY HSPLIT = master2 master3.state = write master3.prev_state = read master3.HWDATA = 1 slave.state = read slave.prev_state = write arbiter.master3_prev_state = transmit -> State: 1.18 <- HWDATA = 0 HRDATA = 1 HSPLIT = 0 master3.state = read master3.prev_state = write master3.HWDATA = 0 slave.state = write slave.prev_state = read slave.MASK_MASTER2 = 0 slave.extended = 1 arbiter.lasterror = 1 -> State: 1.19 <- HWDATA = 1 HRDATA = 0 HRESP = OK master3.state = write master3.prev_state = read master3.HWDATA = 1 slave.state = read slave.prev_state = write slave.extended = 0 -> State: 1.20 <- HTRANS = IDLE HWDATA = 0 HRESP = SPLIT master3.state = idle master3.prev_state = write master3.HTRANS = IDLE master3.HWDATA = 0 slave.state = idle slave.prev_state = read arbiter.lasterror = 0 -> State: 1.21 <- BUSREQ1 = 1 HGRANT3 = 0 HMASTER = default master1.state = busreq master3.prev_state = idle slave.prev_state = idle slave.MASK_MASTER3 = 1 slave.extended = 1 arbiter.master3_state = mask arbiter.lasterror = 1 arbiter.preferred = default -> State: 1.22 <- HREADY = 0 HRESP = OK BUSREQ3 = 1 master1.prev_state = busreq master3.state = busreq slave.extended = 0 arbiter.master3_prev_state = mask -> State: 1.23 <- HREADY = 1 master3.prev_state = busreq arbiter.lasterror = 0 -- Loop starts here -> State: 1.24 <- HREADY = 0 -> State: 1.25 <- HREADY = 1 -> State: 1.26 <- HREADY = 0 ###################################################################### Runtime Statistics ------------------ Machine name: node-xeon-8 User time 780.600 seconds System time 0.830 seconds Average resident text size = 0K Average resident data+stack size = 0K Maximum resident size = 0K Virtual text size = 132044K Virtual data size = 42601K data size initialized = 234K data size uninitialized = 362K data size sbrk = 42005K Virtual memory limit = 4194304K (4194304K) Major page faults = 406 Minor page faults = 55681 Swaps = 0 Input blocks = 0 Output blocks = 0 Context switch (voluntary) = 0 Context switch (involuntary) = 0 ###################################################################### BDD statistics -------------------- BDD nodes allocated: 290545 -------------------- BDD nodes representing init set of states: 44 BDD nodes representing state constraints: 8024 BDD nodes representing input constraints: 1 Forward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 2163 cluster 3 : 1927 cluster 4 : 4667 Backward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 2163 cluster 3 : 1927 cluster 4 : 4667