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