| I2C Hardware/Software Model (46609 lines of code, unwind loop 16) | ||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Property | Result | No. of Constraints | No. of Clauses | No. of Variables | Runtime Decision Procedure | Runtime Total | ||||||||||||||||||
| I2C.1 | Pass | 159481 | 20020885 | 7339850 | 417.878s | 13m23.886s | ||||||||||||||||||
| I2C.1 (unfixed) | Pass | 159744 | 19840615 | 7351520 | 430.849s | 13m59.182s | ||||||||||||||||||
| I2C.2 | Pass | 158391 | 19997082 | 7325831 | 413.127s | 13m13.083s | ||||||||||||||||||
| I2C.2 (unfixed) | Pass | 158654 | 19816812 | 7337501 | 415.806s | 13m15.252s | ||||||||||||||||||
| I2C.3 | Pass | 158556 | 20006113 | 7330617 | 418.215s | 13m15.815s | ||||||||||||||||||
| I2C.3 (unfixed) | Pass | 158819 | 19824200 | 7342354 | 420.652s | 13m14.180s | ||||||||||||||||||
| I2C.4 | Pass | 158556 | 20023452 | 7337759 | 416.02s | 13m7.066s | ||||||||||||||||||
| I2C.4 (unfixed) | Pass | 158819 | 19841537 | 7349496 | 420.589s | 13m18.512s | ||||||||||||||||||
| I2C.5 | Pass | 158556 | 20024494 | 7338044 | 414.27s | 13m6.194s | ||||||||||||||||||
| I2C.5 (unfixed) | Pass | 158819 | 19842551 | 7349781 | 424.977s | 13m39.940s | ||||||||||||||||||
| I2C.6 | Pass | 158436 | 19998982 | 7327197 | 415.978s | 13m3.400s | ||||||||||||||||||
| I2C.6 (unfixed) | Pass | 158699 | 19818647 | 7338867 | 419.162s | 13m25.647s | ||||||||||||||||||
| I2C.7 | Pass | 158436 | 20007984 | 7330738 | 414.037s | 13m6.050s | ||||||||||||||||||
| I2C.7 (unfixed) | Pass | 158699 | 19827649 | 7342408 | 416.23s | 13m8.062s | ||||||||||||||||||
| I2C.8 | Pass | 158436 | 20001601 | 7327333 | 412.863s | 13m0.486s | ||||||||||||||||||
| I2C.8 (unfixed) | Pass | 158699 | 19821266 | 7339003 | 417.481s | 13m17.503s | ||||||||||||||||||
| I2C.9 | Pass | 163866 | 20118277 | 7387280 | 449.291s | 14m14.420s | ||||||||||||||||||
| I2C.9 (unfixed) | Pass | 164144 | 19924513 | 7399382 | 466.109s | 14m31.211s | ||||||||||||||||||
| I2C.10 | Pass | 164547 | 20074751 | 7395672 | 432.06s | 14m1.016s | ||||||||||||||||||
| I2C.10 (unfixed) | Pass | 164810 | 19892935 | 7407563 | 438.244s | 14m15.764s | ||||||||||||||||||
| I2C.11 | Pass | 162381 | 20388706 | 7480868 | 433.704s | 13m28.636s | ||||||||||||||||||
| I2C.11 (unfixed) | Pass | 162644 | 20079411 | 7492508 | 438.425s | 13m47.399s | ||||||||||||||||||
| I2C.12 | Pass | 158556 | 20160928 | 7381603 | 418.607s | 13m9.419s | ||||||||||||||||||
| I2C.12 (unfixed) | Pass | 158819 | 19918604 | 7393408 | 420.884s | 13m16.875s | ||||||||||||||||||
| I2C.13 | Pass | 158811 | 20009910 | 7332076 | 423.026s | 13m24.312s | ||||||||||||||||||
| I2C.13 (unfixed) | Pass | 159074 | 19827807 | 7343833 | 438.502s | 13m42.182s | ||||||||||||||||||
| I2C.14 | Pass | 160596 | 20294436 | 7495055 | 421.973s | 13m18.677s | ||||||||||||||||||
| I2C.14 (unfixed) | Pass | 160859 | 20098988 | 7506796 | 440.324s | 14m15.961s | ||||||||||||||||||
| I2C.15 | Pass | 160596 | 20295406 | 7495337 | 421.739s | 13m20.781s | ||||||||||||||||||
| I2C.15 (unfixed) | Pass | 160859 | 20100004 | 7507072 | 425.796s | 13m32.659s | ||||||||||||||||||
| I2C.16 | Pass | 158391 | 19997740 | 7326173 | 413.214s | 13m8.866s | ||||||||||||||||||
| I2C.16 (unfixed) | Pass | 158654 | 19817320 | 7337852 | 428.915s | 13m37.658s | ||||||||||||||||||
| I2C.17 | Pass | 167481 | 20064678 | 7341968 | 460.146s | 15m12.867s | ||||||||||||||||||
| I2C.17 (unfixed) | Pass | 167744 | 19875712 | 7353727 | 456.228s | 14m59.372s | ||||||||||||||||||
| I2C QEMU Hardware Model (684 lines of code, unwind loop 4) | ||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Property | Result | No. of Constraints | No. of Clauses | No. of Variables | Runtime Decision Procedure | Runtime Total | ||||||||||||||||||
| I2C.1 | Pass | 8703 | 181485 | 107104 | 1.407s | 0m3.609s | ||||||||||||||||||
| I2C.1 (unfixed) | Pass | 8202 | 165311 | 105380 | 1.273s | 0m3.367s | ||||||||||||||||||
| I2C.2 | Pass | 8493 | 177322 | 104986 | 1.37s | 0m3.504s | ||||||||||||||||||
| I2C.2 (unfixed) | Pass | 8007 | 161484 | 103413 | 1.243s | 0m3.286s | ||||||||||||||||||
| I2C.3 | Pass | 8503 | 176311 | 104953 | 1.372s | 0m3.514s | ||||||||||||||||||
| I2C.3 (unfixed) | Pass | 8021 | 160558 | 103384 | 1.236s | 0m3.278s | ||||||||||||||||||
| I2C.4 | Pass | 8525 | 179389 | 105503 | 1.395s | 0m3.537s | ||||||||||||||||||
| I2C.4 (unfixed) | Pass | 8043 | 163564 | 103934 | 1.25s | 0m3.300s | ||||||||||||||||||
| I2C.5 | Pass | 8525 | 179437 | 105513 | 1.398s | 0m3.535s | ||||||||||||||||||
| I2C.5 (unfixed) | Pass | 8043 | 163612 | 103944 | 1.449s | 0m3.555s | ||||||||||||||||||
| I2C.6 | Pass | 8537 | 178192 | 105029 | 1.388s | 0m3.530s | ||||||||||||||||||
| I2C.6 (unfixed) | Pass | 8051 | 162320 | 103456 | 1.25s | 0m3.309s | ||||||||||||||||||
| I2C.7 | Pass | 8537 | 179572 | 105713 | 1.397s | 0m3.545s | ||||||||||||||||||
| I2C.7 (unfixed) | Pass | 8051 | 163647 | 104128 | 1.252s | 0m3.309s | ||||||||||||||||||
| I2C.8 | Pass | 8537 | 179232 | 105054 | 1.432s | 0m3.553s | ||||||||||||||||||
| I2C.8 (unfixed) | Pass | 8051 | 163297 | 103480 | 1.267s | 0m3.368s | ||||||||||||||||||
| I2C.9 (SW Only) | N/A | N/A | N/A | N/A | N/A | N/A | ||||||||||||||||||
| I2C.10 | Pass | 9050 | 182631 | 108850 | 1.489s | 0m3.821s | ||||||||||||||||||
| I2C.10 (unfixed) | Failed | 8564 | 166646 | 107234 | 1.365s | 0m3.641s | ||||||||||||||||||
| I2C.11 | Pass | 9053 | 199697 | 117187 | 1.554s | 0m3.840s | ||||||||||||||||||
| I2C.11 (unfixed) | Pass | 8571 | 180950 | 115618 | 1.382s | 0m3.600s | ||||||||||||||||||
| I2C.12 | Pass | 8525 | 181863 | 108755 | 1.418s | 0m3.578s | ||||||||||||||||||
| I2C.12 (unfixed) | Pass | 8043 | 164217 | 107186 | 1.285s | 0m3.435s | ||||||||||||||||||
| I2C.13 | Pass | 8613 | 180449 | 105183 | 1.416s | 0m3.606s | ||||||||||||||||||
| I2C.13 (unfixed) | Pass | 8131 | 164580 | 103614 | 1.293s | 0m3.415s | ||||||||||||||||||
| I2C.14 | Pass | 8701 | 192844 | 119177 | 1.432s | 0m3.599s | ||||||||||||||||||
| I2C.14 (unfixed) | Pass | 8219 | 176312 | 117608 | 1.277s | 0m3.347s | ||||||||||||||||||
| I2C.15 | Pass | 8701 | 192932 | 119187 | 1.431s | 0m3.615s | ||||||||||||||||||
| I2C.15 (unfixed) | Pass | 8219 | 176366 | 117618 | 1.283s | 0m3.361s | ||||||||||||||||||
| I2C.16 | Pass | 8493 | 177356 | 105034 | 1.368s | 0m3.489s | ||||||||||||||||||
| I2C.16 (unfixed) | Pass | 8007 | 161508 | 103457 | 1.265s | 0m3.328s | ||||||||||||||||||
| I2C.17 | Pass | 9397 | 189018 | 106090 | 1.552s | 0m4.012s | ||||||||||||||||||
| I2C.17 (unfixed) | Pass | 8915 | 172671 | 104521 | 1.414s | 0m3.748s | ||||||||||||||||||
| I2C.18 | Pass | 8441 | 176386 | 104944 | 1.368s | 0m3.489s | ||||||||||||||||||
| I2C.18 (unfixed) | Failed | 7959 | 160615 | 103375 | 1.276s | 0m3.424s | ||||||||||||||||||
| I2C.19 | Pass | 8441 | 176459 | 104953 | 1.364s | 0m3.490s | ||||||||||||||||||
| I2C.19 (unfixed) | Pass | 7959 | 160686 | 103384 | 1.26s | 0m3.318s | ||||||||||||||||||
| I2C.20 | Pass | 8441 | 176495 | 104953 | 1.364s | 0m3.483s | ||||||||||||||||||
| I2C.20 (unfixed) | Pass | 7959 | 160722 | 103384 | 1.252s | 0m3.292s | ||||||||||||||||||