| RTC Hardware/Software Model (47609 lines of code, unwind loop 21) | ||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Property | Result | No. of Constraints | No. of Clauses | No. of Variables | Runtime Decision Procedure | Runtime Total | ||||||||||||||||||
| RTC.1 | Pass | 61314 | 25797536 | 8917160 | 67.663s | 2m2.497s | ||||||||||||||||||
| RTC.1 (unfixed) | Failed | 61065 | 25771226 | 8901239 | 177.352s | 3m45.268s | ||||||||||||||||||
| RTC.2 | Pass | 61314 | 26430338 | 9140440 | 19.281s | 1m11.653s | ||||||||||||||||||
| RTC.2 (unfixed) | Pass | 61065 | 26403464 | 9124218 | 19.303s | 1m10.062s | ||||||||||||||||||
| RTC.3 | Pass | 60648 | 25769903 | 8913869 | 18.737s | 1m8.537s | ||||||||||||||||||
| RTC.3 (unfixed) | Pass | 60399 | 25743651 | 8898038 | 18.525s | 1m11.430s | ||||||||||||||||||
| RTC.4 | Pass | 60766 | 26422852 | 9136690 | 19.423s | 1m9.654s | ||||||||||||||||||
| RTC.4 (unfixed) | Pass | 60517 | 26395978 | 9120468 | 19.173s | 1m10.774s | ||||||||||||||||||
| RTC.5 | Pass | 60435 | 26425148 | 9133887 | 18.884s | 1m9.494s | ||||||||||||||||||
| RTC.5 (unfixed) | Pass | 60186 | 26398274 | 9117665 | 18.895s | 1m10.208s | ||||||||||||||||||
| RTC.6 | Pass | 60295 | 8208764 | 2819538 | 4.556s | 0m54.136s | ||||||||||||||||||
| RTC.6 (unfixed) | Pass | 60046 | 8200865 | 2814273 | 4.551s | 0m52.702s | ||||||||||||||||||
| RTC.7 | Pass | 60394 | 8759757 | 3004628 | 4.77s | 0m55.205s | ||||||||||||||||||
| RTC.7 (unfixed) | Pass | 60145 | 8751259 | 2998972 | 4.767s | 0m54.128s | ||||||||||||||||||
| RTC.8 | Pass | 60294 | 24491011 | 8463827 | 17.255s | 1m9.055s | ||||||||||||||||||
| RTC.8 (unfixed) | Pass | 60045 | 24465993 | 8448779 | 17.218s | 1m7.884s | ||||||||||||||||||
| RTC.9 | Pass | 60294 | 24468704 | 8463868 | 17.236s | 1m7.665s | ||||||||||||||||||
| RTC.9 (unfixed) | Pass | 60045 | 24443686 | 8448820 | 17.165s | 1m6.689s | ||||||||||||||||||
| RTC.10 | Pass | 60294 | 24781142 | 8572052 | 17.534s | 1m8.610s | ||||||||||||||||||
| RTC.10 (unfixed) | Pass | 60045 | 24755818 | 8556808 | 17.463s | 1m7.760s | ||||||||||||||||||
| RTC.11 | Pass | 60668 | 25231840 | 8718844 | 58.963s | 1m52.783s | ||||||||||||||||||
| RTC.11 (unfixed) | Pass | 60419 | 25206208 | 8703404 | 58.666s | 1m50.010s | ||||||||||||||||||
| RTC QEMU Hardware Model (1485 lines of code, unwind loop 11 for Prop 1 & 2, and 1 for the rest) | ||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Property | Result | No. of Constraints | No. of Clauses | No. of Variables | Runtime Decision Procedure | Runtime Total | ||||||||||||||||||
| RTC.1 | Pass | 58605 | 26136568 | 8910882 | 66.092s | 2m4.271s | ||||||||||||||||||
| RTC.1 (unfixed) | Failed | 24029 | 10180429 | 3475849 | 39.563s | 0m49.990s | ||||||||||||||||||
| RTC.2 | Pass | 58605 | 26772974 | 9132347 | 21.064s | 1m20.584s | ||||||||||||||||||
| RTC.2 (unfixed) | Pass | 24029 | 10829048 | 3696758 | 6.176s | 0m15.874s | ||||||||||||||||||
| RTC.3 | Pass | 57153 | 26754219 | 9122440 | 20.4s | 1m16.104s | ||||||||||||||||||
| RTC.3 (unfixed) | Pass | 23351 | 10822120 | 3692903 | 6.131s | 0m15.528s | ||||||||||||||||||
| RTC.4 | Pass | 56890 | 26753313 | 9121994 | 21.519s | 1m13.105s | ||||||||||||||||||
| RTC.4 (unfixed) | Pass | 23238 | 10821848 | 3692723 | 6.127s | 0m15.520s | ||||||||||||||||||
| RTC.5 | Pass | 56933 | 26755420 | 9119008 | 21.021s | 1m18.661s | ||||||||||||||||||
| RTC.5 (unfixed) | Pass | 23260 | 10821688 | 3691529 | 6.118s | 0m15.596s | ||||||||||||||||||
| RTC.6 | Pass | 56749 | 26752805 | 9121907 | 20.689s | 1m20.954s | ||||||||||||||||||
| RTC.6 (unfixed) | Pass | 23177 | 10821606 | 3692677 | 6.128s | 0m15.625s | ||||||||||||||||||
| RTC.7 | Pass | 56821 | 26744792 | 9114308 | 20.259s | 1m16.474s | ||||||||||||||||||
| RTC.7 (unfixed) | Pass | 23193 | 10819191 | 3690965 | 6.158s | 0m15.819s | ||||||||||||||||||
| RTC.8 | Pass | 56797 | 26752762 | 9121916 | 21.589s | 1m14.647s | ||||||||||||||||||
| RTC.8 (unfixed) | Pass | 23203 | 10821647 | 3692691 | 6.243s | 0m16.147s | ||||||||||||||||||
| RTC.9 | Pass | 56797 | 26752806 | 9121938 | 20.843s | 1m18.580s | ||||||||||||||||||
| RTC.9 (unfixed) | Pass | 23203 | 10821667 | 3692701 | 6.238s | 0m16.124s | ||||||||||||||||||
| RTC.10 | Pass | 56797 | 26752828 | 9121938 | 20.875s | 1m21.256s | ||||||||||||||||||
| RTC.10 (unfixed) | Pass | 23203 | 10821677 | 3692701 | 6.236s | 0m16.110s | ||||||||||||||||||
| RTC.11 | Pass | 57185 | 26796853 | 9127454 | 78.632s | 2m11.345s | ||||||||||||||||||
| RTC.11 (unfixed) | Pass | 23371 | 10836330 | 3694769 | 27.473s | 0m37.653s | ||||||||||||||||||