amba10b4unrealn.aag

aag 1107 42 73 1 992
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52
54
56
58
60
62
64
66
68
70
72
74
76
78
80
82
84
86 1
88 58
90 36
92 1561
94 60
96 38
98 64
100 1575
102 1589
104 1635
106 66
108 1649
110 1663
112 68
114 1677
116 8
118 70
120 1691
122 72
124 74
126 1775
128 1789
130 1801
132 1825
134 1845
136 46
138 84
140 42
142 1869
144 1883
146 40
148 1933
150 1939
152 1945
154 34
156 82
158 1959
160 1981
162 30
164 2003
166 2033
168 80
170 2047
172 28
174 2069
176 78
178 62
180 24
182 2091
184 48
186 76
188 44
190 20
192 2113
194 4
196 2127
198 16
200 2149
202 10
204 12
206 2
208 2171
210 14
212 275
214 2193
216 18
218 2215
220 22
222 54
224 26
226 56
228 32
230 6
1358
232 55 12
234 57 16
236 235 233
238 59 20
240 239 236
242 61 24
244 243 240
246 65 28
248 247 244
250 67 30
252 251 248
254 69 34
256 255 252
258 71 40
260 259 256
262 73 42
264 263 260
266 75 46
268 267 264
270 213 86
272 271 86
274 273 268
276 83 81
278 276 79
280 278 77
282 54 45
284 55 44
286 285 283
288 287 280
290 82 81
292 290 79
294 292 77
296 56 45
298 57 44
300 299 297
302 301 294
304 303 289
306 83 80
308 306 79
310 308 77
312 58 45
314 59 44
316 315 313
318 317 310
320 319 304
322 82 80
324 322 79
326 324 77
328 60 45
330 61 44
332 331 329
334 333 326
336 335 320
338 276 78
340 338 77
342 64 45
344 65 44
346 345 343
348 347 340
350 349 336
352 290 78
354 352 77
356 66 45
358 67 44
360 359 357
362 361 354
364 363 350
366 306 78
368 366 77
370 68 45
372 69 44
374 373 371
376 375 368
378 377 364
380 322 78
382 380 77
384 70 45
386 71 44
388 387 385
390 389 382
392 391 378
394 278 76
396 72 45
398 73 44
400 399 397
402 401 394
404 403 392
406 292 76
408 74 45
410 75 44
412 411 409
414 413 406
416 415 404
418 185 86
420 184 86
422 419 86
424 423 9
426 425 416
428 167 86
430 166 86
432 429 86
434 430 9
436 435 426
438 127 86
440 126 86
442 439 86
444 133 86
446 132 86
448 445 86
450 449 443
452 135 86
454 134 86
456 453 86
458 457 450
460 459 9
462 461 436
464 207 86
466 206 86
468 465 86
470 466 280
472 469 281
474 473 471
476 475 420
478 477 462
480 195 86
482 194 86
484 481 86
486 485 294
488 482 295
490 489 487
492 491 420
494 493 478
496 203 86
498 202 86
500 497 86
502 501 310
504 498 311
506 505 503
508 507 420
510 509 494
512 211 86
514 210 86
516 513 86
518 517 326
520 514 327
522 521 519
524 523 420
526 525 510
528 217 86
530 216 86
532 529 86
534 533 340
536 530 341
538 537 535
540 539 420
542 541 526
544 221 86
546 220 86
548 545 86
550 549 354
552 546 355
554 553 551
556 555 420
558 557 542
560 225 86
562 224 86
564 561 86
566 565 368
568 562 369
570 569 567
572 571 420
574 573 558
576 229 86
578 228 86
580 577 86
582 581 382
584 578 383
586 585 583
588 587 420
590 589 574
592 91 86
594 90 86
596 593 86
598 597 394
600 594 395
602 601 599
604 603 420
606 605 590
608 97 86
610 96 86
612 609 86
614 613 406
616 610 407
618 617 615
620 619 420
622 621 606
624 231 86
626 230 86
628 625 86
630 626 85
632 629 84
634 633 631
636 635 420
638 637 622
640 157 86
642 156 86
644 641 86
646 169 86
648 168 86
650 647 86
652 651 645
654 177 86
656 176 86
658 655 86
660 659 652
662 187 86
664 186 86
666 663 86
668 667 660
670 669 280
672 668 281
674 673 671
676 675 8
678 677 638
680 651 642
682 680 659
684 682 667
686 685 294
688 684 295
690 689 687
692 691 8
694 693 678
696 648 645
698 696 659
700 698 667
702 701 310
704 700 311
706 705 703
708 707 8
710 709 694
712 648 642
714 712 659
716 714 667
718 717 326
720 716 327
722 721 719
724 723 8
726 725 710
728 656 652
730 728 667
732 731 340
734 730 341
736 735 733
738 737 8
740 739 726
742 680 656
744 742 667
746 745 354
748 744 355
750 749 747
752 751 8
754 753 740
756 696 656
758 756 667
760 759 368
762 758 369
764 763 761
766 765 8
768 767 754
770 712 656
772 770 667
774 773 382
776 772 383
778 777 775
780 779 8
782 781 768
784 664 660
786 785 394
788 784 395
790 789 787
792 791 8
794 793 782
796 682 664
798 797 406
800 796 407
802 801 799
804 803 8
806 805 794
808 139 86
810 138 86
812 809 86
814 813 84
816 810 85
818 817 815
820 819 8
822 821 806
824 179 86
826 178 86
828 825 86
830 205 86
832 204 86
834 831 86
836 832 829
838 836 3
840 838 7
842 841 822
844 835 829
846 844 3
848 846 6
850 849 842
852 199 86
854 198 86
856 853 86
858 854 829
860 858 4
862 860 7
864 863 850
866 857 829
868 866 4
870 868 6
872 871 864
874 191 86
876 190 86
878 875 86
880 876 829
882 880 10
884 882 7
886 885 872
888 879 829
890 888 10
892 890 6
894 893 886
896 181 86
898 180 86
900 897 86
902 898 829
904 902 14
906 904 7
908 907 894
910 901 829
912 910 14
914 912 6
916 915 908
918 173 86
920 172 86
922 919 86
924 920 829
926 924 18
928 926 7
930 929 916
932 923 829
934 932 18
936 934 6
938 937 930
940 163 86
942 162 86
944 941 86
946 942 829
948 946 22
950 948 7
952 951 938
954 945 829
956 954 22
958 956 6
960 959 952
962 155 86
964 154 86
966 963 86
968 964 829
970 968 26
972 970 7
974 973 960
976 967 829
978 976 26
980 978 6
982 981 974
984 147 86
986 146 86
988 985 86
990 986 829
992 990 32
994 992 7
996 995 982
998 989 829
1000 998 32
1002 1000 6
1004 1003 996
1006 141 86
1008 140 86
1010 1007 86
1012 1008 829
1014 1012 36
1016 1014 7
1018 1017 1004
1020 1011 829
1022 1020 36
1024 1022 6
1026 1025 1018
1028 137 86
1030 136 86
1032 1029 86
1034 1030 829
1036 1034 38
1038 1036 7
1040 1039 1026
1042 1033 829
1044 1042 38
1046 1044 6
1048 1047 1040
1050 469 2
1052 466 3
1054 1053 1051
1056 1055 826
1058 1057 1048
1060 482 5
1062 485 4
1064 1063 1061
1066 1065 826
1068 1067 1058
1070 498 11
1072 501 10
1074 1073 1071
1076 1075 826
1078 1077 1068
1080 514 15
1082 517 14
1084 1083 1081
1086 1085 826
1088 1087 1078
1090 530 19
1092 533 18
1094 1093 1091
1096 1095 826
1098 1097 1088
1100 546 23
1102 549 22
1104 1103 1101
1106 1105 826
1108 1107 1098
1110 562 27
1112 565 26
1114 1113 1111
1116 1115 826
1118 1117 1108
1120 578 33
1122 581 32
1124 1123 1121
1126 1125 826
1128 1127 1118
1130 594 37
1132 597 36
1134 1133 1131
1136 1135 826
1138 1137 1128
1140 610 39
1142 613 38
1144 1143 1141
1146 1145 826
1148 1147 1138
1150 626 7
1152 629 6
1154 1153 1151
1156 1155 826
1158 1157 1148
1160 161 86
1162 160 86
1164 1161 86
1166 57 4
1168 1166 1162
1170 1169 1158
1172 165 86
1174 164 86
1176 1173 86
1178 59 10
1180 1178 1174
1182 1181 1170
1184 175 86
1186 174 86
1188 1185 86
1190 61 14
1192 1190 1186
1194 1193 1182
1196 183 86
1198 182 86
1200 1197 86
1202 65 18
1204 1202 1198
1206 1205 1194
1208 193 86
1210 192 86
1212 1209 86
1214 67 22
1216 1214 1210
1218 1217 1206
1220 201 86
1222 200 86
1224 1221 86
1226 69 26
1228 1226 1222
1230 1229 1218
1232 209 86
1234 208 86
1236 1233 86
1238 71 32
1240 1238 1234
1242 1241 1230
1244 215 86
1246 214 86
1248 1245 86
1250 73 36
1252 1250 1246
1254 1253 1242
1256 219 86
1258 218 86
1260 1257 86
1262 75 38
1264 1262 1258
1266 1265 1254
1268 223 86
1270 1269 86
1272 227 86
1274 1273 86
1276 1275 1271
1278 89 86
1280 1279 86
1282 1281 1276
1284 95 86
1286 1285 86
1288 1287 1282
1290 99 86
1292 1291 86
1294 1293 1288
1296 107 86
1298 1297 86
1300 1299 1294
1302 113 86
1304 1303 86
1306 1305 1300
1308 119 86
1310 1309 86
1312 1311 1306
1314 123 86
1316 1315 86
1318 1317 1312
1320 125 86
1322 1321 86
1324 1323 1318
1326 1324 829
1328 1326 2
1330 1329 1266
1332 153 86
1334 152 86
1336 1333 86
1338 151 86
1340 150 86
1342 1339 86
1344 149 86
1346 148 86
1348 1345 86
1350 1347 1341
1352 1350 1336
1354 1353 1337
1356 1354 1330
1358 1357 274
1360 197 86
1362 196 86
1364 1361 86
1366 1365 430
1368 171 86
1370 170 86
1372 1369 86
1374 1373 459
1376 1375 1367
1378 159 86
1380 158 86
1382 1379 86
1384 281 54
1386 1384 1383
1388 1387 1376
1390 145 86
1392 144 86
1394 1391 86
1396 295 56
1398 1396 1395
1400 1399 1388
1402 129 86
1404 128 86
1406 1403 86
1408 311 58
1410 1408 1407
1412 1411 1400
1414 121 86
1416 120 86
1418 1415 86
1420 327 60
1422 1420 1419
1424 1423 1412
1426 111 86
1428 110 86
1430 1427 86
1432 341 64
1434 1432 1431
1436 1435 1424
1438 101 86
1440 100 86
1442 1439 86
1444 355 66
1446 1444 1443
1448 1447 1436
1450 93 86
1452 92 86
1454 1451 86
1456 369 68
1458 1456 1455
1460 1459 1448
1462 103 86
1464 102 86
1466 1463 86
1468 383 70
1470 1468 1467
1472 1471 1460
1474 109 86
1476 108 86
1478 1475 86
1480 395 72
1482 1480 1479
1484 1483 1472
1486 115 86
1488 114 86
1490 1487 86
1492 407 74
1494 1492 1491
1496 1495 1484
1498 1365 433
1500 1373 458
1502 1501 1499
1504 1385 1383
1506 1505 1502
1508 1397 1395
1510 1509 1506
1512 1409 1407
1514 1513 1510
1516 1421 1419
1518 1517 1514
1520 1433 1431
1522 1521 1518
1524 1445 1443
1526 1525 1522
1528 1457 1455
1530 1529 1526
1532 1469 1467
1534 1533 1530
1536 1481 1479
1538 1537 1534
1540 1493 1491
1542 1541 1538
1544 1543 1497
1546 1545 1497
1548 1543 1459
1550 1542 1452
1552 1551 1549
1554 1553 1497
1556 1554 1547
1558 1546 1452
1560 1559 1557
1562 1543 1447
1564 1542 1440
1566 1565 1563
1568 1567 1497
1570 1568 1547
1572 1546 1440
1574 1573 1571
1576 1543 1471
1578 1542 1464
1580 1579 1577
1582 1581 1497
1584 1582 1547
1586 1546 1464
1588 1587 1585
1590 131 86
1592 130 86
1594 1591 86
1596 143 86
1598 142 86
1600 1597 86
1602 1598 1595
1604 105 86
1606 104 86
1608 1605 86
1610 1609 49
1612 1611 1603
1614 1542 1497
1616 1614 1612
1618 1617 1546
1620 1614 1613
1622 1621 1618
1624 1613 1611
1626 1624 1542
1628 1626 1497
1630 1628 1623
1632 1622 1606
1634 1633 1631
1636 1543 1483
1638 1542 1476
1640 1639 1637
1642 1641 1497
1644 1642 1547
1646 1546 1476
1648 1647 1645
1650 1543 1435
1652 1542 1428
1654 1653 1651
1656 1655 1497
1658 1656 1547
1660 1546 1428
1662 1661 1659
1664 1543 1495
1666 1542 1488
1668 1667 1665
1670 1669 1497
1672 1670 1547
1674 1546 1488
1676 1675 1673
1678 1543 1423
1680 1542 1416
1682 1681 1679
1684 1683 1497
1686 1684 1547
1688 1546 1416
1690 1689 1687
1692 458 84
1694 1692 9
1696 1694 53
1698 1696 50
1700 1698 49
1702 1698 48
1704 449 440
1706 1704 457
1708 1706 48
1710 446 443
1712 1710 457
1714 1712 48
1716 446 440
1718 1716 457
1720 1718 48
1722 454 450
1724 1722 48
1726 1702 1701
1728 1727 1701
1730 1703 1701
1732 1730 1708
1734 1733 1728
1736 1730 1709
1738 1736 1714
1740 1739 1734
1742 1736 1715
1744 1742 1720
1746 1745 1740
1748 1742 1721
1750 1748 1724
1752 1751 1746
1754 1725 440
1756 1754 1721
1758 1756 1715
1760 1759 1715
1762 1761 1709
1764 1762 1703
1766 1764 1701
1768 1767 1701
1770 1769 1753
1772 1752 440
1774 1773 1771
1776 1543 1411
1778 1542 1404
1780 1779 1777
1782 1781 1497
1784 1782 1547
1786 1546 1404
1788 1787 1785
1790 1613 1603
1792 1790 1542
1794 1792 1497
1796 1794 1623
1798 1622 1592
1800 1799 1797
1802 1725 446
1804 1802 1721
1806 1804 1715
1808 1807 1715
1810 1809 1709
1812 1811 1709
1814 1813 1703
1816 1815 1703
1818 1817 1701
1820 1818 1753
1822 1752 446
1824 1823 1821
1826 1725 454
1828 1826 1721
1830 1829 1721
1832 1831 1715
1834 1832 1709
1836 1834 1703
1838 1836 1701
1840 1838 1753
1842 1752 454
1844 1843 1841
1846 1601 84
1848 1846 53
1850 1848 51
1852 1598 45
1854 1852 1851
1856 1855 1851
1858 1853 1598
1860 1858 1851
1862 1861 1851
1864 1863 1857
1866 1856 1598
1868 1867 1865
1870 1543 1399
1872 1542 1392
1874 1873 1871
1876 1875 1497
1878 1876 1547
1880 1546 1392
1882 1881 1879
1884 1612 1349
1886 1613 1346
1888 1887 1885
1890 1889 1542
1892 1890 1497
1894 1346 1343
1896 1347 1340
1898 1897 1895
1900 1899 1612
1902 1613 1340
1904 1903 1901
1906 1905 1542
1908 1906 1497
1910 1346 1340
1912 1910 1337
1914 1911 1334
1916 1915 1913
1918 1917 1612
1920 1613 1334
1922 1921 1919
1924 1923 1542
1926 1924 1497
1928 1892 1619
1930 1618 1346
1932 1931 1929
1934 1908 1619
1936 1618 1340
1938 1937 1935
1940 1926 1619
1942 1618 1334
1944 1943 1941
1946 1543 1387
1948 1542 1380
1950 1949 1947
1952 1951 1497
1954 1952 1547
1956 1546 1380
1958 1957 1955
1960 1165 5
1962 1960 57
1964 1162 56
1966 1964 1963
1968 1967 1963
1970 1965 1162
1972 1970 1963
1974 1973 1963
1976 1975 1969
1978 1968 1162
1980 1979 1977
1982 1177 11
1984 1982 59
1986 1174 58
1988 1986 1985
1990 1989 1985
1992 1987 1174
1994 1992 1985
1996 1995 1985
1998 1997 1991
2000 1990 1174
2002 2001 1999
2004 84 9
2006 2004 53
2008 2006 51
2010 2008 433
2012 430 45
2014 2013 2011
2016 2009 430
2018 2017 2009
2020 430 44
2022 2019 433
2024 2020 430
2026 2025 2023
2028 2027 2015
2030 2014 430
2032 2031 2029
2034 1543 1375
2036 1542 1370
2038 2037 2035
2040 2039 1497
2042 2040 1547
2044 1546 1370
2046 2045 2043
2048 1189 15
2050 2048 61
2052 1186 60
2054 2052 2051
2056 2055 2051
2058 2053 1186
2060 2058 2051
2062 2061 2051
2064 2063 2057
2066 2056 1186
2068 2067 2065
2070 1201 19
2072 2070 65
2074 1198 64
2076 2074 2073
2078 2077 2073
2080 2075 1198
2082 2080 2073
2084 2083 2073
2086 2085 2079
2088 2078 1198
2090 2089 2087
2092 1213 23
2094 2092 67
2096 1210 66
2098 2096 2095
2100 2099 2095
2102 2097 1210
2104 2102 2095
2106 2105 2095
2108 2107 2101
2110 2100 1210
2112 2111 2109
2114 1543 1367
2116 1542 1362
2118 2117 2115
2120 2119 1497
2122 2120 1547
2124 1546 1362
2126 2125 2123
2128 1225 27
2130 2128 69
2132 1222 68
2134 2132 2131
2136 2135 2131
2138 2133 1222
2140 2138 2131
2142 2141 2131
2144 2143 2137
2146 2136 1222
2148 2147 2145
2150 1237 33
2152 2150 71
2154 1234 70
2156 2154 2153
2158 2157 2153
2160 2155 1234
2162 2160 2153
2164 2163 2153
2166 2165 2159
2168 2158 1234
2170 2169 2167
2172 1249 37
2174 2172 73
2176 1246 72
2178 2176 2175
2180 2179 2175
2182 2177 1246
2184 2182 2175
2186 2185 2175
2188 2187 2181
2190 2180 1246
2192 2191 2189
2194 1261 39
2196 2194 75
2198 1258 74
2200 2198 2197
2202 2201 2197
2204 2199 1258
2206 2204 2197
2208 2207 2197
2210 2209 2203
2212 2202 1258
2214 2213 2211
i0 controllable_nhgrant0
i1 controllable_hgrant1
i2 controllable_locked
i3 controllable_nstart
i4 controllable_hgrant2
i5 i_hlock0
i6 controllable_hgrant3
i7 i_hlock1
i8 controllable_hgrant4
i9 i_hlock2
i10 controllable_hgrant5
i11 i_hlock3
i12 controllable_hgrant6
i13 i_hlock4
i14 i_hlock5
i15 controllable_hgrant7
i16 i_hlock6
i17 controllable_hgrant8
i18 controllable_hgrant9
i19 i_hlock7
i20 i_hlock8
i21 controllable_busreq
i22 i_hlock9
i23 i_hready
i24 i_hburst1
i25 i_hburst0
i26 i_hbusreq0
i27 i_hbusreq1
i28 i_hbusreq2
i29 i_hbusreq3
i30 controllable_ndecide
i31 i_hbusreq4
i32 i_hbusreq5
i33 i_hbusreq6
i34 i_hbusreq7
i35 i_hbusreq8
i36 i_hbusreq9
i37 controllable_hmaster3
i38 controllable_hmaster2
i39 controllable_hmaster1
i40 controllable_hmaster0
i41 controllable_hmastlock
l0 n87
l1 reg_i_hbusreq2_out
l2 reg_controllable_hgrant8_out
l3 sys_fair8done_out
l4 reg_i_hbusreq3_out
l5 reg_controllable_hgrant9_out
l6 reg_i_hbusreq4_out
l7 sys_fair7done_out
l8 sys_fair9done_out
l9 env_fair1done_out
l10 reg_i_hbusreq5_out
l11 sys_fair10done_out
l12 sys_fair6done_out
l13 reg_i_hbusreq6_out
l14 sys_fair11done_out
l15 reg_controllable_nstart_out
l16 reg_i_hbusreq7_out
l17 sys_fair5done_out
l18 reg_i_hbusreq8_out
l19 reg_i_hbusreq9_out
l20 reg_stateG3_0_out
l21 sys_fair4done_out
l22 env_fair0done_out
l23 reg_stateG3_1_out
l24 reg_stateG3_2_out
l25 reg_i_hlock9_out
l26 reg_controllable_hmastlock_out
l27 reg_i_hlock8_out
l28 reg_stateA1_out
l29 sys_fair3done_out
l30 reg_i_hlock7_out
l31 fair_cnt<0>_out
l32 fair_cnt<1>_out
l33 fair_cnt<2>_out
l34 reg_i_hlock6_out
l35 reg_controllable_hmaster0_out
l36 sys_fair2done_out
l37 reg_stateG10_1_out
l38 reg_i_hlock5_out
l39 reg_stateG10_2_out
l40 reg_stateG2_out
l41 reg_controllable_hmaster1_out
l42 sys_fair1done_out
l43 reg_i_hlock4_out
l44 reg_stateG10_3_out
l45 reg_controllable_hmaster2_out
l46 reg_controllable_ndecide_out
l47 reg_i_hlock3_out
l48 reg_stateG10_4_out
l49 reg_i_hready_out
l50 reg_controllable_hmaster3_out
l51 reg_controllable_busreq_out
l52 reg_i_hlock2_out
l53 reg_stateG10_5_out
l54 reg_controllable_hgrant1_out
l55 sys_fair0done_out
l56 reg_i_hlock1_out
l57 reg_stateG10_6_out
l58 reg_controllable_hgrant2_out
l59 reg_i_hlock0_out
l60 reg_controllable_nhgrant0_out
l61 reg_stateG10_7_out
l62 reg_controllable_hgrant3_out
l63 env_safe_err_happened_out
l64 reg_stateG10_8_out
l65 reg_controllable_hgrant4_out
l66 reg_stateG10_9_out
l67 reg_controllable_hgrant5_out
l68 reg_i_hbusreq0_out
l69 reg_controllable_hgrant6_out
l70 reg_i_hbusreq1_out
l71 reg_controllable_hgrant7_out
l72 reg_controllable_locked_out
o0 o_err
c
amba_10_new_4
This file was written by ABC on Sat Aug 31 20:24:52 2013
For information about AIGER format, refer to http://fmv.jku.at/aiger
-------------------------------
This AIGER file has been created by the following sequence of commands:
> vl2mv amba10b4unreal.v   ---gives--> amba10b4unreal.mv
> abc -c "read_blif_mv amba10b4unreal.mv; write_aiger -s amba10b4unrealn.aig"   ---gives--> amba10b4unrealn.aig
> aigtoaig amba10b4unrealn.aig amba10b4unrealn.aag   ---gives--> amba10b4unrealn.aag (this file)
Content of amba10b4unreal.v:
module amba_10_new_4(
        o_err,
        i_clk,
        i_hready,
        i_hbusreq0,
        i_hlock0,
        i_hbusreq1,
        i_hlock1,
        i_hbusreq2,
        i_hlock2,
        i_hbusreq3,
        i_hlock3,
        i_hbusreq4,
        i_hlock4,
        i_hbusreq5,
        i_hlock5,
        i_hbusreq6,
        i_hlock6,
        i_hbusreq7,
        i_hlock7,
        i_hbusreq8,
        i_hlock8,
        i_hbusreq9,
        i_hlock9,
        i_hburst0,
        i_hburst1,
        controllable_hmaster0,
        controllable_hmaster1,
        controllable_hmaster2,
        controllable_hmaster3,
        controllable_hmastlock,
        controllable_nstart,
        controllable_ndecide,
        controllable_locked,
        controllable_nhgrant0,
        controllable_hgrant1,
        controllable_hgrant2,
        controllable_hgrant3,
        controllable_hgrant4,
        controllable_hgrant5,
        controllable_hgrant6,
        controllable_hgrant7,
        controllable_hgrant8,
        controllable_hgrant9,
        controllable_busreq);

input i_clk;
input i_hready;
input i_hbusreq0;
input i_hlock0;
input i_hbusreq1;
input i_hlock1;
input i_hbusreq2;
input i_hlock2;
input i_hbusreq3;
input i_hlock3;
input i_hbusreq4;
input i_hlock4;
input i_hbusreq5;
input i_hlock5;
input i_hbusreq6;
input i_hlock6;
input i_hbusreq7;
input i_hlock7;
input i_hbusreq8;
input i_hlock8;
input i_hbusreq9;
input i_hlock9;
input i_hburst0;
input i_hburst1;
input controllable_hmaster0;
input controllable_hmaster1;
input controllable_hmaster2;
input controllable_hmaster3;
input controllable_hmastlock;
input controllable_nstart;
input controllable_ndecide;
input controllable_locked;
input controllable_nhgrant0;
input controllable_hgrant1;
input controllable_hgrant2;
input controllable_hgrant3;
input controllable_hgrant4;
input controllable_hgrant5;
input controllable_hgrant6;
input controllable_hgrant7;
input controllable_hgrant8;
input controllable_hgrant9;
input controllable_busreq;
output o_err;

reg reg_i_hready;
reg reg_i_hbusreq0;
reg reg_i_hlock0;
reg reg_i_hbusreq1;
reg reg_i_hlock1;
reg reg_i_hbusreq2;
reg reg_i_hlock2;
reg reg_i_hbusreq3;
reg reg_i_hlock3;
reg reg_i_hbusreq4;
reg reg_i_hlock4;
reg reg_i_hbusreq5;
reg reg_i_hlock5;
reg reg_i_hbusreq6;
reg reg_i_hlock6;
reg reg_i_hbusreq7;
reg reg_i_hlock7;
reg reg_i_hbusreq8;
reg reg_i_hlock8;
reg reg_i_hbusreq9;
reg reg_i_hlock9;
reg reg_controllable_hmaster0;
reg reg_controllable_hmaster1;
reg reg_controllable_hmaster2;
reg reg_controllable_hmaster3;
reg reg_controllable_hmastlock;
reg reg_controllable_nstart;
reg reg_controllable_ndecide;
reg reg_controllable_locked;
reg reg_controllable_nhgrant0;
reg reg_controllable_hgrant1;
reg reg_controllable_hgrant2;
reg reg_controllable_hgrant3;
reg reg_controllable_hgrant4;
reg reg_controllable_hgrant5;
reg reg_controllable_hgrant6;
reg reg_controllable_hgrant7;
reg reg_controllable_hgrant8;
reg reg_controllable_hgrant9;
reg reg_controllable_busreq;
reg reg_stateA1;
reg reg_stateG2;
reg reg_stateG3_0;
reg reg_stateG3_1;
reg reg_stateG3_2;
reg reg_stateG10_1;
reg reg_stateG10_2;
reg reg_stateG10_3;
reg reg_stateG10_4;
reg reg_stateG10_5;
reg reg_stateG10_6;
reg reg_stateG10_7;
reg reg_stateG10_8;
reg reg_stateG10_9;
reg env_safe_err_happened;
reg env_fair0done;
reg env_fair1done;
reg sys_fair0done;
reg sys_fair1done;
reg sys_fair2done;
reg sys_fair3done;
reg sys_fair4done;
reg sys_fair5done;
reg sys_fair6done;
reg sys_fair7done;
reg sys_fair8done;
reg sys_fair9done;
reg sys_fair10done;
reg sys_fair11done;
reg [2:0] fair_cnt;

wire env_safe_err0;
wire env_safe_err1;
wire env_safe_err2;
wire env_safe_err3;
wire env_safe_err4;
wire env_safe_err5;
wire env_safe_err6;
wire env_safe_err7;
wire env_safe_err8;
wire env_safe_err9;
wire env_safe_err;

wire sys_safe_err0;
wire sys_safe_err1;
wire sys_safe_err2;
wire sys_safe_err3;
wire sys_safe_err4;
wire sys_safe_err5;
wire sys_safe_err6;
wire sys_safe_err7;
wire sys_safe_err8;
wire sys_safe_err9;
wire sys_safe_err10;
wire sys_safe_err11;
wire sys_safe_err12;
wire sys_safe_err13;
wire sys_safe_err14;
wire sys_safe_err15;
wire sys_safe_err16;
wire sys_safe_err17;
wire sys_safe_err18;
wire sys_safe_err19;
wire sys_safe_err20;
wire sys_safe_err21;
wire sys_safe_err22;
wire sys_safe_err23;
wire sys_safe_err24;
wire sys_safe_err25;
wire sys_safe_err26;
wire sys_safe_err27;
wire sys_safe_err28;
wire sys_safe_err29;
wire sys_safe_err30;
wire sys_safe_err31;
wire sys_safe_err32;
wire sys_safe_err33;
wire sys_safe_err34;
wire sys_safe_err35;
wire sys_safe_err36;
wire sys_safe_err37;
wire sys_safe_err38;
wire sys_safe_err39;
wire sys_safe_err40;
wire sys_safe_err41;
wire sys_safe_err42;
wire sys_safe_err43;
wire sys_safe_err44;
wire sys_safe_err45;
wire sys_safe_err46;
wire sys_safe_err47;
wire sys_safe_err48;
wire sys_safe_err49;
wire sys_safe_err50;
wire sys_safe_err51;
wire sys_safe_err52;
wire sys_safe_err53;
wire sys_safe_err54;
wire sys_safe_err55;
wire sys_safe_err56;
wire sys_safe_err57;
wire sys_safe_err58;
wire sys_safe_err59;
wire sys_safe_err60;
wire sys_safe_err61;
wire sys_safe_err62;
wire sys_safe_err63;
wire sys_safe_err64;
wire sys_safe_err65;
wire sys_safe_err66;
wire sys_safe_err67;
wire sys_safe_err68;
wire sys_safe_err69;
wire sys_safe_err70;
wire sys_safe_err71;
wire sys_safe_err72;
wire sys_safe_err73;
wire sys_safe_err74;
wire sys_safe_err75;
wire sys_safe_err;

wire env_fair0;
wire env_fair1;

wire sys_fair0;
wire sys_fair1;
wire sys_fair2;
wire sys_fair3;
wire sys_fair4;
wire sys_fair5;
wire sys_fair6;
wire sys_fair7;
wire sys_fair8;
wire sys_fair9;
wire sys_fair10;
wire sys_fair11;
wire progress_in_sys_fair;
wire all_env_fair_fulfilled;
wire all_sys_fair_fulfilled;
wire fair_err;
wire o_err;

// =============================================================
//                        ENV_TRANSITION:
// =============================================================
// Assumption 3:
// G( hlock0=1 -> hbusreq0=1 );
assign env_safe_err0 =  ~(~ i_hlock0 | i_hbusreq0);

// Assumption 3:
// G( hlock1=1 -> hbusreq1=1 );
assign env_safe_err1 =  ~(~ i_hlock1 | i_hbusreq1);

// Assumption 3:
// G( hlock2=1 -> hbusreq2=1 );
assign env_safe_err2 =  ~(~ i_hlock2 | i_hbusreq2);

// Assumption 3:
// G( hlock3=1 -> hbusreq3=1 );
assign env_safe_err3 =  ~(~ i_hlock3 | i_hbusreq3);

// Assumption 3:
// G( hlock4=1 -> hbusreq4=1 );
assign env_safe_err4 =  ~(~ i_hlock4 | i_hbusreq4);

// Assumption 3:
// G( hlock5=1 -> hbusreq5=1 );
assign env_safe_err5 =  ~(~ i_hlock5 | i_hbusreq5);

// Assumption 3:
// G( hlock6=1 -> hbusreq6=1 );
assign env_safe_err6 =  ~(~ i_hlock6 | i_hbusreq6);

// Assumption 3:
// G( hlock7=1 -> hbusreq7=1 );
assign env_safe_err7 =  ~(~ i_hlock7 | i_hbusreq7);

// Assumption 3:
// G( hlock8=1 -> hbusreq8=1 );
assign env_safe_err8 =  ~(~ i_hlock8 | i_hbusreq8);

// Assumption 3:
// G( hlock9=1 -> hbusreq9=1 );
assign env_safe_err9 =  ~(~ i_hlock9 | i_hbusreq9);

// collecting together the safety error bits:
assign env_safe_err = env_safe_err0 |
                      env_safe_err1 |
                      env_safe_err2 |
                      env_safe_err3 |
                      env_safe_err4 |
                      env_safe_err5 |
                      env_safe_err6 |
                      env_safe_err7 |
                      env_safe_err8 |
                      env_safe_err9;

// =============================================================
//                        SYS_TRANSITION:
// =============================================================
// G((hmaster0=0) * (hmaster1=0) * (hmaster2=0) * (hmaster3=0) -> (hbusreq0=0 <-> busreq=0));
assign sys_safe_err0 =  ~( ~( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) )|(~i_hbusreq0 ^~ (~controllable_busreq)));

// G((hmaster0=1) * (hmaster1=0) * (hmaster2=0) * (hmaster3=0) -> (hbusreq1=0 <-> busreq=0));
assign sys_safe_err1 =  ~( ~( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) )|(~i_hbusreq1 ^~ (~controllable_busreq)));

// G((hmaster0=0) * (hmaster1=1) * (hmaster2=0) * (hmaster3=0) -> (hbusreq2=0 <-> busreq=0));
assign sys_safe_err2 =  ~( ~( ~(controllable_hmaster0) & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) )|(~i_hbusreq2 ^~ (~controllable_busreq)));

// G((hmaster0=1) * (hmaster1=1) * (hmaster2=0) * (hmaster3=0) -> (hbusreq3=0 <-> busreq=0));
assign sys_safe_err3 =  ~( ~( controllable_hmaster0 & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) )|(~i_hbusreq3 ^~ (~controllable_busreq)));

// G((hmaster0=0) * (hmaster1=0) * (hmaster2=1) * (hmaster3=0) -> (hbusreq4=0 <-> busreq=0));
assign sys_safe_err4 =  ~( ~( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) )|(~i_hbusreq4 ^~ (~controllable_busreq)));

// G((hmaster0=1) * (hmaster1=0) * (hmaster2=1) * (hmaster3=0) -> (hbusreq5=0 <-> busreq=0));
assign sys_safe_err5 =  ~( ~( controllable_hmaster0 & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) )|(~i_hbusreq5 ^~ (~controllable_busreq)));

// G((hmaster0=0) * (hmaster1=1) * (hmaster2=1) * (hmaster3=0) -> (hbusreq6=0 <-> busreq=0));
assign sys_safe_err6 =  ~( ~( ~(controllable_hmaster0) & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) )|(~i_hbusreq6 ^~ (~controllable_busreq)));

// G((hmaster0=1) * (hmaster1=1) * (hmaster2=1) * (hmaster3=0) -> (hbusreq7=0 <-> busreq=0));
assign sys_safe_err7 =  ~( ~( controllable_hmaster0 & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) )|(~i_hbusreq7 ^~ (~controllable_busreq)));

// G((hmaster0=0) * (hmaster1=0) * (hmaster2=0) * (hmaster3=1) -> (hbusreq8=0 <-> busreq=0));
assign sys_safe_err8 =  ~( ~( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 )|(~i_hbusreq8 ^~ (~controllable_busreq)));

// G((hmaster0=1) * (hmaster1=0) * (hmaster2=0) * (hmaster3=1) -> (hbusreq9=0 <-> busreq=0));
assign sys_safe_err9 =  ~( ~( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 )|(~i_hbusreq9 ^~ (~controllable_busreq)));

// Guarantee 1:
// G((hready=0) -> X(start=0));
assign sys_safe_err10 =  ~( reg_i_hready | controllable_nstart );

// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err11 =  ~( ~(reg_stateG2 & ~controllable_nstart) | 0 );

// G(((stateG3_0=1) * (stateG3_1=0) * (stateG3_2=0) * ((start=1))) -> FALSE);
// G(((stateG3_0=0) * (stateG3_1=1) * (stateG3_2=0) * ((start=1))) -> FALSE);
// G(((stateG3_0=1) * (stateG3_1=1) * (stateG3_2=0) * ((start=1))) -> FALSE);
// G(((stateG3_0=0) * (stateG3_1=0) * (stateG3_2=1) * ((start=1))) -> FALSE);
// all these rules can be summarized as: only in state 000, start=1 is allowed:
assign sys_safe_err12 =  (reg_stateG3_0 | reg_stateG3_1 | reg_stateG3_2) & ~controllable_nstart;

// G( (hready=1) -> (   (hgrant0=1) <-> (X(hmaster0=0) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=0))  ) );
assign sys_safe_err13 =  ~( ~(reg_i_hready) | ( ~reg_controllable_nhgrant0 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant1=1) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=0))  ) );
assign sys_safe_err14 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant1 ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant2=1) <-> (X(hmaster0=0) * X(hmaster1=1) * X(hmaster2=0) * X(hmaster3=0))  ) );
assign sys_safe_err15 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant2 ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant3=1) <-> (X(hmaster0=1) * X(hmaster1=1) * X(hmaster2=0) * X(hmaster3=0))  ) );
assign sys_safe_err16 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant3 ^~ ( controllable_hmaster0 & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant4=1) <-> (X(hmaster0=0) * X(hmaster1=0) * X(hmaster2=1) * X(hmaster3=0))  ) );
assign sys_safe_err17 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant4 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant5=1) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=1) * X(hmaster3=0))  ) );
assign sys_safe_err18 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant5 ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant6=1) <-> (X(hmaster0=0) * X(hmaster1=1) * X(hmaster2=1) * X(hmaster3=0))  ) );
assign sys_safe_err19 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant6 ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant7=1) <-> (X(hmaster0=1) * X(hmaster1=1) * X(hmaster2=1) * X(hmaster3=0))  ) );
assign sys_safe_err20 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant7 ^~ ( controllable_hmaster0 & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) ) ) );

// G( (hready=1) -> (   (hgrant8=1) <-> (X(hmaster0=0) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=1))  ) );
assign sys_safe_err21 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant8 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 ) ) );

// G( (hready=1) -> (   (hgrant9=1) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=1))  ) );
assign sys_safe_err22 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant9 ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 ) ) );

// HMASTLOCK:
// G(  (hready=1) -> (locked=0 <-> X(hmastlock=0) ) );
assign sys_safe_err23 =  ~( ~(reg_i_hready) | (~reg_controllable_locked ^~ ~controllable_hmastlock) );

// Master 0:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=0) * (hmaster2=0) * (hmaster3=0)) <-> (X(hmaster0=0) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=0)) ) );
assign sys_safe_err24 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) & ~(reg_controllable_hmaster2) & ~(reg_controllable_hmaster3) ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) )) );

// Master 1:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=0) * (hmaster2=0) * (hmaster3=0)) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=0)) ) );
assign sys_safe_err25 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & ~(reg_controllable_hmaster1) & ~(reg_controllable_hmaster2) & ~(reg_controllable_hmaster3) ) ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) )) );

// Master 2:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=1) * (hmaster2=0) * (hmaster3=0)) <-> (X(hmaster0=0) * X(hmaster1=1) * X(hmaster2=0) * X(hmaster3=0)) ) );
assign sys_safe_err26 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & reg_controllable_hmaster1 & ~(reg_controllable_hmaster2) & ~(reg_controllable_hmaster3) ) ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) )) );

// Master 3:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=1) * (hmaster2=0) * (hmaster3=0)) <-> (X(hmaster0=1) * X(hmaster1=1) * X(hmaster2=0) * X(hmaster3=0)) ) );
assign sys_safe_err27 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & reg_controllable_hmaster1 & ~(reg_controllable_hmaster2) & ~(reg_controllable_hmaster3) ) ^~ ( controllable_hmaster0 & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) )) );

// Master 4:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=0) * (hmaster2=1) * (hmaster3=0)) <-> (X(hmaster0=0) * X(hmaster1=0) * X(hmaster2=1) * X(hmaster3=0)) ) );
assign sys_safe_err28 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) & reg_controllable_hmaster2 & ~(reg_controllable_hmaster3) ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) )) );

// Master 5:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=0) * (hmaster2=1) * (hmaster3=0)) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=1) * X(hmaster3=0)) ) );
assign sys_safe_err29 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & ~(reg_controllable_hmaster1) & reg_controllable_hmaster2 & ~(reg_controllable_hmaster3) ) ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) )) );

// Master 6:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=1) * (hmaster2=1) * (hmaster3=0)) <-> (X(hmaster0=0) * X(hmaster1=1) * X(hmaster2=1) * X(hmaster3=0)) ) );
assign sys_safe_err30 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & reg_controllable_hmaster1 & reg_controllable_hmaster2 & ~(reg_controllable_hmaster3) ) ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) )) );

// Master 7:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=1) * (hmaster2=1) * (hmaster3=0)) <-> (X(hmaster0=1) * X(hmaster1=1) * X(hmaster2=1) * X(hmaster3=0)) ) );
assign sys_safe_err31 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & reg_controllable_hmaster1 & reg_controllable_hmaster2 & ~(reg_controllable_hmaster3) ) ^~ ( controllable_hmaster0 & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) )) );

// Master 8:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=0) * (hmaster2=0) * (hmaster3=1)) <-> (X(hmaster0=0) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=1)) ) );
assign sys_safe_err32 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) & ~(reg_controllable_hmaster2) & reg_controllable_hmaster3 ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 )) );

// Master 9:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=0) * (hmaster2=0) * (hmaster3=1)) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=0) * X(hmaster3=1)) ) );
assign sys_safe_err33 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & ~(reg_controllable_hmaster1) & ~(reg_controllable_hmaster2) & reg_controllable_hmaster3 ) ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 )) );

// Guarantee 6.2:
// G( ((X(start=0))) -> ( (hmastlock=1) <-> X(hmastlock=1)) );
assign sys_safe_err34 =  ~( ~(controllable_nstart) | ( reg_controllable_hmastlock ^~ controllable_hmastlock) );

// G( (decide=1  *  hlock0=1  *  X(hgrant0=1) )->X(locked=1));
assign sys_safe_err35 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock0 & ~controllable_nhgrant0) | (controllable_locked) );

// G((decide=1  *  hlock0=0  *  X(hgrant0=1))->X(locked=0));
assign sys_safe_err36 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock0 & ~controllable_nhgrant0) | (~controllable_locked) );

// G( (decide=1  *  hlock1=1  *  X(hgrant1=1) )->X(locked=1));
assign sys_safe_err37 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock1 & controllable_hgrant1) | (controllable_locked) );

// G((decide=1  *  hlock1=0  *  X(hgrant1=1))->X(locked=0));
assign sys_safe_err38 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock1 & controllable_hgrant1) | (~controllable_locked) );

// G( (decide=1  *  hlock2=1  *  X(hgrant2=1) )->X(locked=1));
assign sys_safe_err39 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock2 & controllable_hgrant2) | (controllable_locked) );

// G((decide=1  *  hlock2=0  *  X(hgrant2=1))->X(locked=0));
assign sys_safe_err40 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock2 & controllable_hgrant2) | (~controllable_locked) );

// G( (decide=1  *  hlock3=1  *  X(hgrant3=1) )->X(locked=1));
assign sys_safe_err41 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock3 & controllable_hgrant3) | (controllable_locked) );

// G((decide=1  *  hlock3=0  *  X(hgrant3=1))->X(locked=0));
assign sys_safe_err42 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock3 & controllable_hgrant3) | (~controllable_locked) );

// G( (decide=1  *  hlock4=1  *  X(hgrant4=1) )->X(locked=1));
assign sys_safe_err43 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock4 & controllable_hgrant4) | (controllable_locked) );

// G((decide=1  *  hlock4=0  *  X(hgrant4=1))->X(locked=0));
assign sys_safe_err44 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock4 & controllable_hgrant4) | (~controllable_locked) );

// G( (decide=1  *  hlock5=1  *  X(hgrant5=1) )->X(locked=1));
assign sys_safe_err45 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock5 & controllable_hgrant5) | (controllable_locked) );

// G((decide=1  *  hlock5=0  *  X(hgrant5=1))->X(locked=0));
assign sys_safe_err46 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock5 & controllable_hgrant5) | (~controllable_locked) );

// G( (decide=1  *  hlock6=1  *  X(hgrant6=1) )->X(locked=1));
assign sys_safe_err47 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock6 & controllable_hgrant6) | (controllable_locked) );

// G((decide=1  *  hlock6=0  *  X(hgrant6=1))->X(locked=0));
assign sys_safe_err48 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock6 & controllable_hgrant6) | (~controllable_locked) );

// G( (decide=1  *  hlock7=1  *  X(hgrant7=1) )->X(locked=1));
assign sys_safe_err49 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock7 & controllable_hgrant7) | (controllable_locked) );

// G((decide=1  *  hlock7=0  *  X(hgrant7=1))->X(locked=0));
assign sys_safe_err50 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock7 & controllable_hgrant7) | (~controllable_locked) );

// G( (decide=1  *  hlock8=1  *  X(hgrant8=1) )->X(locked=1));
assign sys_safe_err51 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock8 & controllable_hgrant8) | (controllable_locked) );

// G((decide=1  *  hlock8=0  *  X(hgrant8=1))->X(locked=0));
assign sys_safe_err52 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock8 & controllable_hgrant8) | (~controllable_locked) );

// G( (decide=1  *  hlock9=1  *  X(hgrant9=1) )->X(locked=1));
assign sys_safe_err53 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock9 & controllable_hgrant9) | (controllable_locked) );

// G((decide=1  *  hlock9=0  *  X(hgrant9=1))->X(locked=0));
assign sys_safe_err54 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock9 & controllable_hgrant9) | (~controllable_locked) );

// G( (decide=0) -> (  ((hgrant0=0)<->X(hgrant0=0))  ));
assign sys_safe_err55 =  ~( ~(reg_controllable_ndecide) | (reg_controllable_nhgrant0 ^~ controllable_nhgrant0) );

// G( (decide=0) -> (  ((hgrant1=0)<->X(hgrant1=0))  ));
assign sys_safe_err56 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant1 ^~ ~controllable_hgrant1) );

// G( (decide=0) -> (  ((hgrant2=0)<->X(hgrant2=0))  ));
assign sys_safe_err57 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant2 ^~ ~controllable_hgrant2) );

// G( (decide=0) -> (  ((hgrant3=0)<->X(hgrant3=0))  ));
assign sys_safe_err58 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant3 ^~ ~controllable_hgrant3) );

// G( (decide=0) -> (  ((hgrant4=0)<->X(hgrant4=0))  ));
assign sys_safe_err59 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant4 ^~ ~controllable_hgrant4) );

// G( (decide=0) -> (  ((hgrant5=0)<->X(hgrant5=0))  ));
assign sys_safe_err60 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant5 ^~ ~controllable_hgrant5) );

// G( (decide=0) -> (  ((hgrant6=0)<->X(hgrant6=0))  ));
assign sys_safe_err61 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant6 ^~ ~controllable_hgrant6) );

// G( (decide=0) -> (  ((hgrant7=0)<->X(hgrant7=0))  ));
assign sys_safe_err62 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant7 ^~ ~controllable_hgrant7) );

// G( (decide=0) -> (  ((hgrant8=0)<->X(hgrant8=0))  ));
assign sys_safe_err63 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant8 ^~ ~controllable_hgrant8) );

// G( (decide=0) -> (  ((hgrant9=0)<->X(hgrant9=0))  ));
assign sys_safe_err64 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant9 ^~ ~controllable_hgrant9) );

// G((decide=0)->(locked=0 <-> X(locked=0)));
assign sys_safe_err65 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_locked ^~ ~controllable_locked) );

// G(((stateG10_1=1) * (((hgrant1=1)) * (hbusreq1=0)))->FALSE);
assign sys_safe_err66 =  ~( ~(reg_stateG10_1 & (controllable_hgrant1 & ~i_hbusreq1)) | 0 );

// G(((stateG10_2=1) * (((hgrant2=1)) * (hbusreq2=0)))->FALSE);
assign sys_safe_err67 =  ~( ~(reg_stateG10_2 & (controllable_hgrant2 & ~i_hbusreq2)) | 0 );

// G(((stateG10_3=1) * (((hgrant3=1)) * (hbusreq3=0)))->FALSE);
assign sys_safe_err68 =  ~( ~(reg_stateG10_3 & (controllable_hgrant3 & ~i_hbusreq3)) | 0 );

// G(((stateG10_4=1) * (((hgrant4=1)) * (hbusreq4=0)))->FALSE);
assign sys_safe_err69 =  ~( ~(reg_stateG10_4 & (controllable_hgrant4 & ~i_hbusreq4)) | 0 );

// G(((stateG10_5=1) * (((hgrant5=1)) * (hbusreq5=0)))->FALSE);
assign sys_safe_err70 =  ~( ~(reg_stateG10_5 & (controllable_hgrant5 & ~i_hbusreq5)) | 0 );

// G(((stateG10_6=1) * (((hgrant6=1)) * (hbusreq6=0)))->FALSE);
assign sys_safe_err71 =  ~( ~(reg_stateG10_6 & (controllable_hgrant6 & ~i_hbusreq6)) | 0 );

// G(((stateG10_7=1) * (((hgrant7=1)) * (hbusreq7=0)))->FALSE);
assign sys_safe_err72 =  ~( ~(reg_stateG10_7 & (controllable_hgrant7 & ~i_hbusreq7)) | 0 );

// G(((stateG10_8=1) * (((hgrant8=1)) * (hbusreq8=0)))->FALSE);
assign sys_safe_err73 =  ~( ~(reg_stateG10_8 & (controllable_hgrant8 & ~i_hbusreq8)) | 0 );

// G(((stateG10_9=1) * (((hgrant9=1)) * (hbusreq9=0)))->FALSE);
assign sys_safe_err74 =  ~( ~(reg_stateG10_9 & (controllable_hgrant9 & ~i_hbusreq9)) | 0 );

// default master
// G((decide=1  *  hbusreq0=0  *  hbusreq1=0  *  hbusreq2=0  *  hbusreq3=0  *  hbusreq4=0  *  hbusreq5=0  *  hbusreq6=0  *  hbusreq7=0  *  hbusreq8=0  *  hbusreq9=0) -> X(hgrant0=1));
assign sys_safe_err75 =  ~( ~(~reg_controllable_ndecide & (~reg_i_hbusreq0 & ~reg_i_hbusreq1 & ~reg_i_hbusreq2 & ~reg_i_hbusreq3 & ~reg_i_hbusreq4 & ~reg_i_hbusreq5 & ~reg_i_hbusreq6 & ~reg_i_hbusreq7 & ~reg_i_hbusreq8 & ~reg_i_hbusreq9)) | (~controllable_nhgrant0) );

// collecting together the safety error bits:
assign sys_safe_err = sys_safe_err0 |
                      sys_safe_err1 |
                      sys_safe_err2 |
                      sys_safe_err3 |
                      sys_safe_err4 |
                      sys_safe_err5 |
                      sys_safe_err6 |
                      sys_safe_err7 |
                      sys_safe_err8 |
                      sys_safe_err9 |
                      sys_safe_err10 |
                      sys_safe_err11 |
                      sys_safe_err12 |
                      sys_safe_err13 |
                      sys_safe_err14 |
                      sys_safe_err15 |
                      sys_safe_err16 |
                      sys_safe_err17 |
                      sys_safe_err18 |
                      sys_safe_err19 |
                      sys_safe_err20 |
                      sys_safe_err21 |
                      sys_safe_err22 |
                      sys_safe_err23 |
                      sys_safe_err24 |
                      sys_safe_err25 |
                      sys_safe_err26 |
                      sys_safe_err27 |
                      sys_safe_err28 |
                      sys_safe_err29 |
                      sys_safe_err30 |
                      sys_safe_err31 |
                      sys_safe_err32 |
                      sys_safe_err33 |
                      sys_safe_err34 |
                      sys_safe_err35 |
                      sys_safe_err36 |
                      sys_safe_err37 |
                      sys_safe_err38 |
                      sys_safe_err39 |
                      sys_safe_err40 |
                      sys_safe_err41 |
                      sys_safe_err42 |
                      sys_safe_err43 |
                      sys_safe_err44 |
                      sys_safe_err45 |
                      sys_safe_err46 |
                      sys_safe_err47 |
                      sys_safe_err48 |
                      sys_safe_err49 |
                      sys_safe_err50 |
                      sys_safe_err51 |
                      sys_safe_err52 |
                      sys_safe_err53 |
                      sys_safe_err54 |
                      sys_safe_err55 |
                      sys_safe_err56 |
                      sys_safe_err57 |
                      sys_safe_err58 |
                      sys_safe_err59 |
                      sys_safe_err60 |
                      sys_safe_err61 |
                      sys_safe_err62 |
                      sys_safe_err63 |
                      sys_safe_err64 |
                      sys_safe_err65 |
                      sys_safe_err66 |
                      sys_safe_err67 |
                      sys_safe_err68 |
                      sys_safe_err69 |
                      sys_safe_err70 |
                      sys_safe_err71 |
                      sys_safe_err72 |
                      sys_safe_err73 |
                      sys_safe_err74 |
                      sys_safe_err75;

// =============================================================
//                          ENV_FAIRNESS:
// =============================================================
// Assumption 1: 
// G(F(stateA1=0));
assign env_fair0 =  ~reg_stateA1;

// Assumption 2:
// G(F(hready=1));
assign env_fair1 =  i_hready;

assign all_env_fair_fulfilled = (env_fair0done | env_fair0) &
                                (env_fair1done | env_fair1);

// =============================================================
//                          SYS_FAIRNESS:
// =============================================================
// Guarantee 2:
// G(F(stateG2=0));
assign sys_fair0 = ~reg_stateG2;

// Guarantee 3:
// G(F((stateG3_0=0)  *  (stateG3_1=0)  *  (stateG3_2=0)));
assign sys_fair1 =  (~reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2);

// G(F(((hmaster0=0) * (hmaster1=0) * (hmaster2=0) * (hmaster3=0))  |  hbusreq0=0));
assign sys_fair2 =  ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) | ~i_hbusreq0;

// G(F(((hmaster0=1) * (hmaster1=0) * (hmaster2=0) * (hmaster3=0))  |  hbusreq1=0));
assign sys_fair3 =  ( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) | ~i_hbusreq1;

// G(F(((hmaster0=0) * (hmaster1=1) * (hmaster2=0) * (hmaster3=0))  |  hbusreq2=0));
assign sys_fair4 =  ( ~(controllable_hmaster0) & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) | ~i_hbusreq2;

// G(F(((hmaster0=1) * (hmaster1=1) * (hmaster2=0) * (hmaster3=0))  |  hbusreq3=0));
assign sys_fair5 =  ( controllable_hmaster0 & controllable_hmaster1 & ~(controllable_hmaster2) & ~(controllable_hmaster3) ) | ~i_hbusreq3;

// G(F(((hmaster0=0) * (hmaster1=0) * (hmaster2=1) * (hmaster3=0))  |  hbusreq4=0));
assign sys_fair6 =  ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) ) | ~i_hbusreq4;

// G(F(((hmaster0=1) * (hmaster1=0) * (hmaster2=1) * (hmaster3=0))  |  hbusreq5=0));
assign sys_fair7 =  ( controllable_hmaster0 & ~(controllable_hmaster1) & controllable_hmaster2 & ~(controllable_hmaster3) ) | ~i_hbusreq5;

// G(F(((hmaster0=0) * (hmaster1=1) * (hmaster2=1) * (hmaster3=0))  |  hbusreq6=0));
assign sys_fair8 =  ( ~(controllable_hmaster0) & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) ) | ~i_hbusreq6;

// G(F(((hmaster0=1) * (hmaster1=1) * (hmaster2=1) * (hmaster3=0))  |  hbusreq7=0));
assign sys_fair9 =  ( controllable_hmaster0 & controllable_hmaster1 & controllable_hmaster2 & ~(controllable_hmaster3) ) | ~i_hbusreq7;

// G(F(((hmaster0=0) * (hmaster1=0) * (hmaster2=0) * (hmaster3=1))  |  hbusreq8=0));
assign sys_fair10 =  ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 ) | ~i_hbusreq8;

// G(F(((hmaster0=1) * (hmaster1=0) * (hmaster2=0) * (hmaster3=1))  |  hbusreq9=0));
assign sys_fair11 =  ( controllable_hmaster0 & ~(controllable_hmaster1) & ~(controllable_hmaster2) & controllable_hmaster3 ) | ~i_hbusreq9;

assign all_sys_fair_fulfilled = (sys_fair0done | sys_fair0) &
                                (sys_fair1done | sys_fair1) &
                                (sys_fair2done | sys_fair2) &
                                (sys_fair3done | sys_fair3) &
                                (sys_fair4done | sys_fair4) &
                                (sys_fair5done | sys_fair5) &
                                (sys_fair6done | sys_fair6) &
                                (sys_fair7done | sys_fair7) &
                                (sys_fair8done | sys_fair8) &
                                (sys_fair9done | sys_fair9) &
                                (sys_fair10done | sys_fair10) &
                                (sys_fair11done | sys_fair11);
assign progress_in_sys_fair = (~sys_fair0done & sys_fair0) |
                                (~sys_fair1done & sys_fair1) |
                                (~sys_fair2done & sys_fair2) |
                                (~sys_fair3done & sys_fair3) |
                                (~sys_fair4done & sys_fair4) |
                                (~sys_fair5done & sys_fair5) |
                                (~sys_fair6done & sys_fair6) |
                                (~sys_fair7done & sys_fair7) |
                                (~sys_fair8done & sys_fair8) |
                                (~sys_fair9done & sys_fair9) |
                                (~sys_fair10done & sys_fair10) |
                                (~sys_fair11done & sys_fair11);
assign fair_err = (fair_cnt >= 3'b100);

// computing the error output bit:
assign o_err = ~env_safe_err & ~env_safe_err_happened & (sys_safe_err | fair_err);

initial
 begin
  reg_i_hready = 0;
  reg_i_hbusreq0 = 0;
  reg_i_hlock0 = 0;
  reg_i_hbusreq1 = 0;
  reg_i_hlock1 = 0;
  reg_i_hbusreq2 = 0;
  reg_i_hlock2 = 0;
  reg_i_hbusreq3 = 0;
  reg_i_hlock3 = 0;
  reg_i_hbusreq4 = 0;
  reg_i_hlock4 = 0;
  reg_i_hbusreq5 = 0;
  reg_i_hlock5 = 0;
  reg_i_hbusreq6 = 0;
  reg_i_hlock6 = 0;
  reg_i_hbusreq7 = 0;
  reg_i_hlock7 = 0;
  reg_i_hbusreq8 = 0;
  reg_i_hlock8 = 0;
  reg_i_hbusreq9 = 0;
  reg_i_hlock9 = 0;
  reg_controllable_hmaster0 = 0;
  reg_controllable_hmaster1 = 0;
  reg_controllable_hmaster2 = 0;
  reg_controllable_hmaster3 = 0;
  reg_controllable_hmastlock = 0;
  reg_controllable_nstart = 0;
  reg_controllable_ndecide = 0;
  reg_controllable_locked = 0;
  reg_controllable_nhgrant0 = 0;
  reg_controllable_hgrant1 = 0;
  reg_controllable_hgrant2 = 0;
  reg_controllable_hgrant3 = 0;
  reg_controllable_hgrant4 = 0;
  reg_controllable_hgrant5 = 0;
  reg_controllable_hgrant6 = 0;
  reg_controllable_hgrant7 = 0;
  reg_controllable_hgrant8 = 0;
  reg_controllable_hgrant9 = 0;
  reg_controllable_busreq = 0;
  reg_stateA1 = 0;
  reg_stateG2 = 0;
  reg_stateG3_0 = 0;
  reg_stateG3_1 = 0;
  reg_stateG3_2 = 0;
  reg_stateG10_1 = 0;
  reg_stateG10_2 = 0;
  reg_stateG10_3 = 0;
  reg_stateG10_4 = 0;
  reg_stateG10_5 = 0;
  reg_stateG10_6 = 0;
  reg_stateG10_7 = 0;
  reg_stateG10_8 = 0;
  reg_stateG10_9 = 0;
  env_safe_err_happened = 0;
  env_fair0done = 0;
  env_fair1done = 0;
  sys_fair0done = 0;
  sys_fair1done = 0;
  sys_fair2done = 0;
  sys_fair3done = 0;
  sys_fair4done = 0;
  sys_fair5done = 0;
  sys_fair6done = 0;
  sys_fair7done = 0;
  sys_fair8done = 0;
  sys_fair9done = 0;
  sys_fair10done = 0;
  sys_fair11done = 0;
  fair_cnt = 0;
 end


always @(posedge i_clk)
 begin
   // We remember if an environment error occurred:
   env_safe_err_happened = env_safe_err_happened | env_safe_err;

   // Updating the fairness counters: 
   if(all_sys_fair_fulfilled)
    begin
      env_fair0done = 0;
      env_fair1done = 0;
      sys_fair0done = 0;
      sys_fair1done = 0;
      sys_fair2done = 0;
      sys_fair3done = 0;
      sys_fair4done = 0;
      sys_fair5done = 0;
      sys_fair6done = 0;
      sys_fair7done = 0;
      sys_fair8done = 0;
      sys_fair9done = 0;
      sys_fair10done = 0;
      sys_fair11done = 0;
      fair_cnt = 0;
    end
   else
    begin
      if(progress_in_sys_fair)
       begin
         env_fair0done = 0;
         env_fair1done = 0;
         fair_cnt = 0;
         sys_fair0done = sys_fair0done | sys_fair0;
         sys_fair1done = sys_fair1done | sys_fair1;
         sys_fair2done = sys_fair2done | sys_fair2;
         sys_fair3done = sys_fair3done | sys_fair3;
         sys_fair4done = sys_fair4done | sys_fair4;
         sys_fair5done = sys_fair5done | sys_fair5;
         sys_fair6done = sys_fair6done | sys_fair6;
         sys_fair7done = sys_fair7done | sys_fair7;
         sys_fair8done = sys_fair8done | sys_fair8;
         sys_fair9done = sys_fair9done | sys_fair9;
         sys_fair10done = sys_fair10done | sys_fair10;
         sys_fair11done = sys_fair11done | sys_fair11;
       end
      else
       begin
         if(all_env_fair_fulfilled)
          begin
            env_fair0done = 0;
            env_fair1done = 0;
            fair_cnt = fair_cnt + 1;
          end
         else
          begin
            env_fair0done = env_fair0done | env_fair0;
            env_fair1done = env_fair1done | env_fair1;
          end
       end
    end

   // Updating the automata: 
   // Automaton A1: 
   if(~reg_stateA1 & controllable_hmastlock & ~i_hburst0 & ~i_hburst1)
    begin
      reg_stateA1 = 1'b1;
    end
   else if(reg_stateA1 & ~controllable_busreq)
    begin
      reg_stateA1 = 1'b0;
    end

   // Automaton G2: 
   if(~reg_stateG2)
    begin
      if(controllable_hmastlock & ~controllable_nstart & ~i_hburst0 & ~i_hburst1)
       begin
         reg_stateG2 = 1'b1;
       end
    end
   else // if(reg_stateG2)
    begin
      if(~controllable_busreq)
       begin
         reg_stateG2 = 1'b0;
       end
    end

   // Automaton G3: 
   if(~reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2 & controllable_hmastlock & ~controllable_nstart &  ~i_hburst0 & i_hburst1 & ~i_hready)
    begin
      reg_stateG3_0 = 1'b1;
      reg_stateG3_1 = 1'b0;
      reg_stateG3_2 = 1'b0;
    end
   else if(~reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2 & controllable_hmastlock & ~controllable_nstart &  ~i_hburst0 & i_hburst1 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b1;
      reg_stateG3_2 = 1'b0;
    end
   else if(reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b1;
      reg_stateG3_2 = 1'b0;
    end
   else if(~reg_stateG3_0 & reg_stateG3_1 & ~reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b1;
      reg_stateG3_1 = 1'b1;
      reg_stateG3_2 = 1'b0;
    end
   else if(reg_stateG3_0 & reg_stateG3_1 & ~reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b0;
      reg_stateG3_2 = 1'b1;
    end
   else if(~reg_stateG3_0 & ~reg_stateG3_1 & reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b0;
      reg_stateG3_2 = 1'b0;
    end

   // Automaton G10_1: 
   if(~reg_stateG10_1 & ~controllable_hgrant1 & ~i_hbusreq1)
    begin
      reg_stateG10_1 = 1'b1;
    end
   else if(reg_stateG10_1 & i_hbusreq1)
    begin
      reg_stateG10_1 = 1'b0;
    end

   // Automaton G10_2: 
   if(~reg_stateG10_2 & ~controllable_hgrant2 & ~i_hbusreq2)
    begin
      reg_stateG10_2 = 1'b1;
    end
   else if(reg_stateG10_2 & i_hbusreq2)
    begin
      reg_stateG10_2 = 1'b0;
    end

   // Automaton G10_3: 
   if(~reg_stateG10_3 & ~controllable_hgrant3 & ~i_hbusreq3)
    begin
      reg_stateG10_3 = 1'b1;
    end
   else if(reg_stateG10_3 & i_hbusreq3)
    begin
      reg_stateG10_3 = 1'b0;
    end

   // Automaton G10_4: 
   if(~reg_stateG10_4 & ~controllable_hgrant4 & ~i_hbusreq4)
    begin
      reg_stateG10_4 = 1'b1;
    end
   else if(reg_stateG10_4 & i_hbusreq4)
    begin
      reg_stateG10_4 = 1'b0;
    end

   // Automaton G10_5: 
   if(~reg_stateG10_5 & ~controllable_hgrant5 & ~i_hbusreq5)
    begin
      reg_stateG10_5 = 1'b1;
    end
   else if(reg_stateG10_5 & i_hbusreq5)
    begin
      reg_stateG10_5 = 1'b0;
    end

   // Automaton G10_6: 
   if(~reg_stateG10_6 & ~controllable_hgrant6 & ~i_hbusreq6)
    begin
      reg_stateG10_6 = 1'b1;
    end
   else if(reg_stateG10_6 & i_hbusreq6)
    begin
      reg_stateG10_6 = 1'b0;
    end

   // Automaton G10_7: 
   if(~reg_stateG10_7 & ~controllable_hgrant7 & ~i_hbusreq7)
    begin
      reg_stateG10_7 = 1'b1;
    end
   else if(reg_stateG10_7 & i_hbusreq7)
    begin
      reg_stateG10_7 = 1'b0;
    end

   // Automaton G10_8: 
   if(~reg_stateG10_8 & ~controllable_hgrant8 & ~i_hbusreq8)
    begin
      reg_stateG10_8 = 1'b1;
    end
   else if(reg_stateG10_8 & i_hbusreq8)
    begin
      reg_stateG10_8 = 1'b0;
    end

   // Automaton G10_9: 
   if(~reg_stateG10_9 & ~controllable_hgrant9 & ~i_hbusreq9)
    begin
      reg_stateG10_9 = 1'b1;
    end
   else if(reg_stateG10_9 & i_hbusreq9)
    begin
      reg_stateG10_9 = 1'b0;
    end

   // Latching the previous input:
   reg_i_hready =  i_hready;
   reg_i_hbusreq0 =  i_hbusreq0;
   reg_i_hlock0 =  i_hlock0;
   reg_i_hbusreq1 =  i_hbusreq1;
   reg_i_hlock1 =  i_hlock1;
   reg_i_hbusreq2 =  i_hbusreq2;
   reg_i_hlock2 =  i_hlock2;
   reg_i_hbusreq3 =  i_hbusreq3;
   reg_i_hlock3 =  i_hlock3;
   reg_i_hbusreq4 =  i_hbusreq4;
   reg_i_hlock4 =  i_hlock4;
   reg_i_hbusreq5 =  i_hbusreq5;
   reg_i_hlock5 =  i_hlock5;
   reg_i_hbusreq6 =  i_hbusreq6;
   reg_i_hlock6 =  i_hlock6;
   reg_i_hbusreq7 =  i_hbusreq7;
   reg_i_hlock7 =  i_hlock7;
   reg_i_hbusreq8 =  i_hbusreq8;
   reg_i_hlock8 =  i_hlock8;
   reg_i_hbusreq9 =  i_hbusreq9;
   reg_i_hlock9 =  i_hlock9;
   reg_controllable_hmaster0 =  controllable_hmaster0;
   reg_controllable_hmaster1 =  controllable_hmaster1;
   reg_controllable_hmaster2 =  controllable_hmaster2;
   reg_controllable_hmaster3 =  controllable_hmaster3;
   reg_controllable_hmastlock =  controllable_hmastlock;
   reg_controllable_nstart =  controllable_nstart;
   reg_controllable_ndecide =  controllable_ndecide;
   reg_controllable_locked =  controllable_locked;
   reg_controllable_nhgrant0 =  controllable_nhgrant0;
   reg_controllable_hgrant1 =  controllable_hgrant1;
   reg_controllable_hgrant2 =  controllable_hgrant2;
   reg_controllable_hgrant3 =  controllable_hgrant3;
   reg_controllable_hgrant4 =  controllable_hgrant4;
   reg_controllable_hgrant5 =  controllable_hgrant5;
   reg_controllable_hgrant6 =  controllable_hgrant6;
   reg_controllable_hgrant7 =  controllable_hgrant7;
   reg_controllable_hgrant8 =  controllable_hgrant8;
   reg_controllable_hgrant9 =  controllable_hgrant9;
   reg_controllable_busreq =  controllable_busreq;

 end
endmodule

-------------------------------