# Nanotrav Version #0.13, Release date 2015/7/15 # nanotrav/nanotrav -p 1 -autodyn -reordering sifting -trav ./nanotrav/mult32a.blif # CUDD Version 3.0.0 BDD reordering with sifting: from 4001 to ... 268 nodes in 0 sec BDD reordering with sifting: from 537 to ... 246 nodes in 0 sec BDD reordering with sifting: from 493 to ... 250 nodes in 0 sec BDD reordering with sifting: from 501 to ... 280 nodes in 0 sec BDD reordering with sifting: from 561 to ... 296 nodes in 0.01 sec Order before final reordering 2 34 33 66 32 65 31 64 63 30 62 29 28 61 27 60 26 59 25 58 24 57 23 56 22 55 21 54 20 53 19 52 51 18 50 17 49 16 48 15 47 14 46 13 45 12 36 3 37 4 38 5 39 6 40 7 41 8 42 9 43 10 44 11 1 Number of inputs = 65 BDD reordering with sifting: from 380 to ... 317 nodes in 0 sec New order 1 2 34 66 33 65 32 64 31 63 30 62 29 61 28 60 27 59 26 58 25 57 24 56 23 55 22 54 21 53 20 52 19 51 18 50 17 49 16 48 15 47 14 46 13 45 12 36 3 4 37 5 38 6 39 7 40 8 41 9 42 10 43 44 11 Building transition relation. Time = 0.01 sec BDD reordering with sifting: from 669 to ... 452 nodes in 0.01 sec @@BDD reordering with sifting: from 939 to ... 705 nodes in 0 sec @@BDD reordering with sifting: from 1443 to ... 847 nodes in 0.02 sec @@BDD reordering with sifting: from 1727 to ... 1076 nodes in 0.01 sec @@@BDD reordering with sifting: from 2185 to ... 770 nodes in 0.01 sec @@@@BDD reordering with sifting: from 1573 to ... 922 nodes in 0.01 sec @@@@BDD reordering with sifting: from 1877 to ... 1013 nodes in 0.01 sec @@@@@BDD reordering with sifting: from 2059 to ... 873 nodes in 0.02 sec @@@@@BDD reordering with sifting: from 1779 to ... 975 nodes in 0.01 sec @@@@@ Transition relation: 1 parts 32 latches 196 nodes Traversing. Time = 0.11 sec S0: 33 nodes 1 leaves 1 minterms From[1]: 33 nodes 1 leaves 2.14748e+09 minterms Reached[1]: 2 nodes 1 leaves 2.14748e+09 minterms 2147483648 2.14748e+09 From[2]: 3 nodes 1 leaves 1.07374e+09 minterms Reached[2]: 3 nodes 1 leaves 3.22123e+09 minterms 3221225472 3.22123e+09 From[3]: 4 nodes 1 leaves 5.36871e+08 minterms Reached[3]: 4 nodes 1 leaves 3.7581e+09 minterms 3758096384 3.7581e+09 From[4]: 5 nodes 1 leaves 2.68435e+08 minterms Reached[4]: 5 nodes 1 leaves 4.02653e+09 minterms 4026531840 4.02653e+09 From[5]: 6 nodes 1 leaves 1.34218e+08 minterms Reached[5]: 6 nodes 1 leaves 4.16075e+09 minterms 4160749568 4.16075e+09 From[6]: 7 nodes 1 leaves 6.71089e+07 minterms Reached[6]: 7 nodes 1 leaves 4.22786e+09 minterms 4227858432 4.22786e+09 From[7]: 8 nodes 1 leaves 3.35544e+07 minterms Reached[7]: 8 nodes 1 leaves 4.26141e+09 minterms 4261412864 4.26141e+09 From[8]: 9 nodes 1 leaves 1.67772e+07 minterms Reached[8]: 9 nodes 1 leaves 4.27819e+09 minterms 4278190080 4.27819e+09 From[9]: 10 nodes 1 leaves 8.38861e+06 minterms Reached[9]: 10 nodes 1 leaves 4.28658e+09 minterms 4286578688 4.28658e+09 From[10]: 11 nodes 1 leaves 4.1943e+06 minterms Reached[10]: 11 nodes 1 leaves 4.29077e+09 minterms 4290772992 4.29077e+09 From[11]: 12 nodes 1 leaves 2.09715e+06 minterms Reached[11]: 12 nodes 1 leaves 4.29287e+09 minterms 4292870144 4.29287e+09 From[12]: 13 nodes 1 leaves 1.04858e+06 minterms Reached[12]: 13 nodes 1 leaves 4.29392e+09 minterms 4293918720 4.29392e+09 From[13]: 14 nodes 1 leaves 524288 minterms Reached[13]: 14 nodes 1 leaves 4.29444e+09 minterms 4294443008 4.29444e+09 From[14]: 15 nodes 1 leaves 262144 minterms Reached[14]: 15 nodes 1 leaves 4.29471e+09 minterms 4294705152 4.29471e+09 From[15]: 16 nodes 1 leaves 131072 minterms Reached[15]: 16 nodes 1 leaves 4.29484e+09 minterms 4294836224 4.29484e+09 From[16]: 17 nodes 1 leaves 65536 minterms Reached[16]: 17 nodes 1 leaves 4.2949e+09 minterms 4294901760 4.2949e+09 From[17]: 18 nodes 1 leaves 32768 minterms Reached[17]: 18 nodes 1 leaves 4.29493e+09 minterms 4294934528 4.29493e+09 From[18]: 19 nodes 1 leaves 16384 minterms Reached[18]: 19 nodes 1 leaves 4.29495e+09 minterms 4294950912 4.29495e+09 From[19]: 20 nodes 1 leaves 8192 minterms Reached[19]: 20 nodes 1 leaves 4.29496e+09 minterms 4294959104 4.29496e+09 From[20]: 21 nodes 1 leaves 4096 minterms Reached[20]: 21 nodes 1 leaves 4.29496e+09 minterms 4294963200 4.29496e+09 From[21]: 22 nodes 1 leaves 2048 minterms Reached[21]: 22 nodes 1 leaves 4.29497e+09 minterms 4294965248 4.29497e+09 From[22]: 23 nodes 1 leaves 1024 minterms Reached[22]: 23 nodes 1 leaves 4.29497e+09 minterms 4294966272 4.29497e+09 From[23]: 24 nodes 1 leaves 512 minterms Reached[23]: 24 nodes 1 leaves 4.29497e+09 minterms 4294966784 4.29497e+09 From[24]: 25 nodes 1 leaves 256 minterms Reached[24]: 25 nodes 1 leaves 4.29497e+09 minterms 4294967040 4.29497e+09 From[25]: 26 nodes 1 leaves 128 minterms Reached[25]: 26 nodes 1 leaves 4.29497e+09 minterms 4294967168 4.29497e+09 From[26]: 27 nodes 1 leaves 64 minterms Reached[26]: 27 nodes 1 leaves 4.29497e+09 minterms 4294967232 4.29497e+09 From[27]: 28 nodes 1 leaves 32 minterms Reached[27]: 28 nodes 1 leaves 4.29497e+09 minterms 4294967264 4.29497e+09 From[28]: 29 nodes 1 leaves 16 minterms Reached[28]: 29 nodes 1 leaves 4.29497e+09 minterms 4294967280 4.29497e+09 From[29]: 30 nodes 1 leaves 8 minterms Reached[29]: 30 nodes 1 leaves 4.29497e+09 minterms 4294967288 4.29497e+09 From[30]: 31 nodes 1 leaves 4 minterms Reached[30]: 31 nodes 1 leaves 4.29497e+09 minterms 4294967292 4.29497e+09 From[31]: 32 nodes 1 leaves 2 minterms Reached[31]: 32 nodes 1 leaves 4.29497e+09 minterms 4294967294 4.29497e+09 From[32]: 33 nodes 1 leaves 1 minterms Reached[32]: 33 nodes 1 leaves 4.29497e+09 minterms 4294967295 4.29497e+09 depth = 32 R: 33 nodes 1 leaves 4.29497e+09 minterms Order at the end of reachability analysis 1 2 34 33 66 32 65 31 64 63 30 29 62 28 61 27 60 59 26 58 25 57 24 56 23 55 22 54 21 20 53 19 52 18 51 17 50 49 16 15 48 14 47 13 46 12 45 11 44 10 43 3 36 4 37 5 38 6 39 7 40 8 41 42 9 **** CUDD modifiable parameters **** Hard limit for cache size: 2796202 Cache hit threshold for resizing: 30% Garbage collection enabled: yes Limit for fast unique table growth: 1677721 Maximum number of variables sifted per reordering: 1000000 Maximum number of variable swaps per reordering: 1000000000 Maximum growth while sifting a variable: 1.2 Dynamic reordering of BDDs enabled: yes Default BDD reordering method: 4 Dynamic reordering of ZDDs enabled: no Default ZDD reordering method: 4 Realignment of ZDDs to BDDs enabled: no Realignment of BDDs to ZDDs enabled: no Dead nodes counted in triggering reordering: no Group checking criterion: 7 Recombination threshold: 0 Symmetry violation threshold: 10 Arc violation threshold: 10 GA population size: 0 Number of crossovers for GA: 0 Next reordering threshold: 2018 **** CUDD non-modifiable parameters **** Memory in use: 4625812 Peak number of nodes: 7154 Peak number of live nodes: 4004 Number of BDD variables: 97 Number of ZDD variables: 0 Number of cache entries: 65536 Number of cache look-ups: 49867 Number of cache hits: 20816 Number of cache insertions: 29312 Number of cache collisions: 1359 Number of cache deletions: 21085 Cache used slots = 17.70% (expected 10.53%) Soft limit for cache size: 100352 Number of buckets in unique table: 25088 Used buckets in unique table: 12.40% (expected 12.44%) Number of BDD and ADD nodes: 3613 Number of ZDD nodes: 0 Number of dead BDD and ADD nodes: 3266 Number of dead ZDD nodes: 0 Total number of nodes allocated: 26901 Total number of nodes reclaimed: 16737 Garbage collections so far: 15 Time for garbage collection: 0.00 sec Reorderings so far: 15 Time for reordering: 0.11 sec Final size: 275 total time = 0.11 sec Runtime Statistics ------------------ Machine name: crozzon User time 0.1 seconds System time 0.0 seconds Average resident text size = 0K Average resident data+stack size = 0K Maximum resident size = 8080K Virtual memory limit = unlimited (unlimited) Major page faults = 0 Minor page faults = 1509 Swaps = 0 Input blocks = 16 Output blocks = 16 Context switch (voluntary) = 1 Context switch (involuntary) = 1