amba4c7n.aag

aag 620 22 38 1 560
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46 1
48 32
50 18
52 36
54 801
56 885
58 20
60 909
62 42
64 929
66 2
68 30
70 12
72 4
74 38
76 959
78 981
80 44
82 34
84 1003
86 1027
88 8
90 6
92 1095
94 1101
96 1107
98 1113
100 28
102 1135
104 1229
106 1235
108 1241
110 10
112 141
114 24
116 40
118 26
120 22
648
122 24 3
124 28 5
126 125 123
128 34 7
130 129 126
132 38 11
134 133 130
136 113 46
138 137 46
140 139 134
142 23 19
144 31 2
146 30 3
148 147 145
150 149 142
152 22 19
154 31 4
156 30 5
158 157 155
160 159 152
162 161 151
164 23 18
166 31 6
168 30 7
170 169 167
172 171 164
174 173 162
176 22 18
178 31 10
180 30 11
182 181 179
184 183 176
186 185 174
188 117 46
190 116 46
192 189 46
194 193 13
196 195 186
198 77 46
200 76 46
202 199 46
204 200 13
206 205 196
208 57 46
210 56 46
212 209 46
214 61 46
216 60 46
218 215 46
220 219 213
222 65 46
224 64 46
226 223 46
228 227 220
230 229 13
232 231 206
234 81 46
236 80 46
238 235 46
240 236 142
242 239 143
244 243 241
246 245 190
248 247 232
250 119 46
252 118 46
254 251 46
256 255 152
258 252 153
260 259 257
262 261 190
264 263 248
266 49 46
268 48 46
270 267 46
272 271 164
274 268 165
276 275 273
278 277 190
280 279 264
282 53 46
284 52 46
286 283 46
288 287 176
290 284 177
292 291 289
294 293 190
296 295 280
298 59 46
300 58 46
302 299 46
304 300 9
306 303 8
308 307 305
310 309 190
312 311 296
314 121 46
316 120 46
318 315 46
320 51 46
322 50 46
324 321 46
326 325 319
328 327 142
330 326 143
332 331 329
334 333 12
336 335 312
338 325 316
340 339 152
342 338 153
344 343 341
346 345 12
348 347 336
350 322 319
352 351 164
354 350 165
356 355 353
358 357 12
360 359 348
362 322 316
364 363 176
366 362 177
368 367 365
370 369 12
372 371 360
374 89 46
376 88 46
378 375 46
380 379 8
382 376 9
384 383 381
386 385 12
388 387 372
390 63 46
392 62 46
394 391 46
396 115 46
398 114 46
400 397 46
402 398 395
404 402 45
406 404 21
408 407 388
410 401 395
412 410 45
414 412 20
416 415 408
418 101 46
420 100 46
422 419 46
424 420 395
426 424 26
428 426 21
430 429 416
432 423 395
434 432 26
436 434 20
438 437 430
440 83 46
442 82 46
444 441 46
446 442 395
448 446 32
450 448 21
452 451 438
454 445 395
456 454 32
458 456 20
460 459 452
462 75 46
464 74 46
466 463 46
468 464 395
470 468 36
472 470 21
474 473 460
476 467 395
478 476 36
480 478 20
482 481 474
484 239 44
486 236 45
488 487 485
490 489 392
492 491 482
494 252 27
496 255 26
498 497 495
500 499 392
502 501 492
504 268 33
506 271 32
508 507 505
510 509 392
512 511 502
514 284 37
516 287 36
518 517 515
520 519 392
522 521 512
524 300 21
526 303 20
528 527 525
530 529 392
532 531 522
534 79 46
536 78 46
538 535 46
540 26 5
542 540 536
544 543 532
546 85 46
548 84 46
550 547 46
552 32 7
554 552 548
556 555 544
558 103 46
560 102 46
562 559 46
564 36 11
566 564 560
568 567 556
570 67 46
572 571 46
574 73 46
576 575 46
578 577 573
580 91 46
582 581 46
584 583 578
586 111 46
588 587 46
590 589 584
592 590 395
594 592 44
596 595 568
598 109 46
600 108 46
602 599 46
604 107 46
606 106 46
608 605 46
610 105 46
612 104 46
614 611 46
616 615 609
618 617 608
620 618 614
622 621 603
624 623 602
626 624 620
628 614 609
630 615 606
632 631 629
634 620 603
636 621 600
638 637 635
640 632 614
642 640 638
644 643 627
646 644 596
648 647 140
650 93 46
652 92 46
654 651 46
656 95 46
658 94 46
660 657 46
662 97 46
664 96 46
666 663 46
668 98 46
670 659 653
672 670 665
674 672 669
676 674 203
678 659 654
680 678 665
682 680 669
684 682 228
686 660 653
688 686 665
690 688 669
692 143 2
694 693 690
696 660 654
698 696 665
700 698 669
702 153 4
704 703 700
706 670 666
708 706 669
710 165 6
712 711 708
714 678 666
716 714 669
718 177 10
720 719 716
722 55 46
724 54 46
726 723 46
728 87 46
730 86 46
732 729 46
734 733 727
736 724 40
738 684 677
740 739 677
742 685 677
744 742 694
746 745 740
748 742 695
750 748 704
752 751 746
754 748 705
756 754 712
758 757 752
760 754 713
762 760 720
764 763 758
766 760 721
768 766 734
770 769 764
772 766 735
774 772 736
776 775 770
778 737 724
780 778 735
782 781 735
784 783 721
786 784 713
788 786 705
790 788 695
792 790 685
794 792 677
796 794 777
798 776 724
800 799 797
802 228 8
804 802 13
806 804 17
808 806 14
810 808 41
812 808 40
814 219 210
816 814 227
818 816 40
820 216 213
822 820 227
824 822 40
826 216 210
828 826 227
830 828 40
832 224 220
834 832 40
836 812 811
838 837 811
840 813 811
842 840 818
844 843 838
846 840 819
848 846 824
850 849 844
852 846 825
854 852 830
856 855 850
858 852 831
860 858 834
862 861 856
864 835 210
866 864 831
868 866 825
870 869 825
872 871 819
874 872 813
876 874 811
878 877 811
880 879 863
882 862 210
884 883 881
886 835 216
888 886 831
890 888 825
892 891 825
894 893 819
896 895 819
898 897 813
900 899 813
902 901 811
904 902 863
906 862 216
908 907 905
910 835 224
912 910 831
914 913 831
916 915 825
918 916 819
920 918 813
922 920 811
924 922 863
926 862 224
928 927 925
930 13 8
932 930 17
934 932 15
936 934 203
938 200 31
940 939 937
942 935 200
944 943 935
946 200 30
948 945 203
950 946 200
952 951 949
954 953 941
956 940 200
958 957 955
960 539 27
962 960 5
964 536 4
966 964 963
968 967 963
970 965 536
972 970 963
974 973 963
976 975 969
978 968 536
980 979 977
982 551 33
984 982 7
986 548 6
988 986 985
990 989 985
992 987 548
994 992 985
996 995 985
998 997 991
1000 990 548
1002 1001 999
1004 733 8
1006 1004 17
1008 1006 15
1010 730 31
1012 1010 1009
1014 1013 1009
1016 1011 730
1018 1016 1009
1020 1019 1009
1022 1021 1015
1024 1014 730
1026 1025 1023
1028 721 652
1030 1028 713
1032 1031 713
1034 1033 705
1036 1034 695
1038 1037 695
1040 1039 685
1042 1040 677
1044 1043 677
1046 721 658
1048 1046 713
1050 1048 705
1052 1050 695
1054 1053 695
1056 1055 685
1058 1057 685
1060 1059 677
1062 721 664
1064 1062 713
1066 1065 713
1068 1067 705
1070 1069 705
1072 1071 695
1074 1072 685
1076 1074 677
1078 721 668
1080 1078 713
1082 1080 705
1084 1082 695
1086 1084 685
1088 1086 677
1090 1045 765
1092 764 652
1094 1093 1091
1096 1060 765
1098 764 658
1100 1099 1097
1102 1076 765
1104 764 664
1106 1105 1103
1108 1088 765
1110 764 668
1112 1111 1109
1114 563 37
1116 1114 11
1118 560 10
1120 1118 1117
1122 1121 1117
1124 1119 560
1126 1124 1117
1128 1127 1117
1130 1129 1123
1132 1122 560
1134 1133 1131
1136 775 764
1138 736 615
1140 737 612
1142 1141 1139
1144 734 612
1146 1143 735
1148 1147 1145
1150 1149 721
1152 1150 713
1154 1152 705
1156 1154 695
1158 1156 685
1160 1158 677
1162 612 609
1164 613 606
1166 1165 1163
1168 1167 736
1170 737 606
1172 1171 1169
1174 734 606
1176 1173 735
1178 1177 1175
1180 1179 721
1182 1180 713
1184 1182 705
1186 1184 695
1188 1186 685
1190 1188 677
1192 612 606
1194 1192 603
1196 1193 600
1198 1197 1195
1200 1199 736
1202 737 600
1204 1203 1201
1206 734 600
1208 1205 735
1210 1209 1207
1212 1211 721
1214 1212 713
1216 1214 705
1218 1216 695
1220 1218 685
1222 1220 677
1224 1160 1137
1226 1136 612
1228 1227 1225
1230 1190 1137
1232 1136 606
1234 1233 1231
1236 1222 1137
1238 1136 600
1240 1239 1237
i0 i_hbusreq0
i1 i_hbusreq1
i2 i_hbusreq2
i3 controllable_hmastlock
i4 i_hbusreq3
i5 controllable_nstart
i6 i_hburst1
i7 i_hburst0
i8 controllable_hmaster1
i9 controllable_locked
i10 controllable_hmaster0
i11 i_hlock0
i12 controllable_hgrant1
i13 i_hlock1
i14 controllable_busreq
i15 controllable_hgrant2
i16 i_hlock2
i17 controllable_hgrant3
i18 i_hlock3
i19 i_hready
i20 controllable_ndecide
i21 controllable_nhgrant0
l0 n47
l1 reg_controllable_hgrant2_out
l2 reg_controllable_hmaster1_out
l3 reg_controllable_hgrant3_out
l4 next_env_fair_out
l5 reg_stateG3_0_out
l6 reg_controllable_locked_out
l7 reg_stateG3_1_out
l8 reg_controllable_ndecide_out
l9 reg_stateG3_2_out
l10 reg_i_hbusreq0_out
l11 reg_controllable_busreq_out
l12 reg_controllable_nstart_out
l13 reg_i_hbusreq1_out
l14 reg_i_hlock3_out
l15 reg_stateG2_out
l16 reg_stateG10_1_out
l17 reg_controllable_nhgrant0_out
l18 reg_i_hlock2_out
l19 reg_stateG10_2_out
l20 reg_stateA1_out
l21 reg_controllable_hmastlock_out
l22 reg_i_hbusreq2_out
l23 next_sys_fair<0>_out
l24 next_sys_fair<1>_out
l25 next_sys_fair<2>_out
l26 next_sys_fair<3>_out
l27 reg_i_hlock1_out
l28 reg_stateG10_3_out
l29 fair_cnt<0>_out
l30 fair_cnt<1>_out
l31 fair_cnt<2>_out
l32 reg_i_hbusreq3_out
l33 env_safe_err_happened_out
l34 reg_i_hlock0_out
l35 reg_i_hready_out
l36 reg_controllable_hgrant1_out
l37 reg_controllable_hmaster0_out
o0 o_err
c
amba_4_new_7
This file was written by ABC on Sat Aug 31 20:24:50 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 amba4c7.v   ---gives--> amba4c7.mv
> abc -c "read_blif_mv amba4c7.mv; write_aiger -s amba4c7n.aig"   ---gives--> amba4c7n.aig
> aigtoaig amba4c7n.aig amba4c7n.aag   ---gives--> amba4c7n.aag (this file)
Content of amba4c7.v:
module amba_4_new_7(
        o_err,
        i_clk,
        i_hready,
        i_hbusreq0,
        i_hlock0,
        i_hbusreq1,
        i_hlock1,
        i_hbusreq2,
        i_hlock2,
        i_hbusreq3,
        i_hlock3,
        i_hburst0,
        i_hburst1,
        controllable_hmaster0,
        controllable_hmaster1,
        controllable_hmastlock,
        controllable_nstart,
        controllable_ndecide,
        controllable_locked,
        controllable_nhgrant0,
        controllable_hgrant1,
        controllable_hgrant2,
        controllable_hgrant3,
        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_hburst0;
input i_hburst1;
input controllable_hmaster0;
input controllable_hmaster1;
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_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_controllable_hmaster0;
reg reg_controllable_hmaster1;
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_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 env_safe_err_happened;
reg next_env_fair;
reg [2:0] fair_cnt;
reg [3:0] next_sys_fair;

wire env_safe_err0;
wire env_safe_err1;
wire env_safe_err2;
wire env_safe_err3;
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_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 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);

// collecting together the safety error bits:
assign env_safe_err = env_safe_err0 |
                      env_safe_err1 |
                      env_safe_err2 |
                      env_safe_err3;

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

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

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

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

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

// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err5 =  ~( ~(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_err6 =  (reg_stateG3_0 | reg_stateG3_1 | reg_stateG3_2) & ~controllable_nstart;

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

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

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

// G( (hready=1) -> (   (hgrant3=1) <-> (X(hmaster0=1) * X(hmaster1=1))  ) );
assign sys_safe_err10 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant3 ^~ ( controllable_hmaster0 & controllable_hmaster1 ) ) );

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

// Master 0:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=0)) <-> (X(hmaster0=0) * X(hmaster1=0)) ) );
assign sys_safe_err12 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) )) );

// Master 1:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=0)) <-> (X(hmaster0=1) * X(hmaster1=0)) ) );
assign sys_safe_err13 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & ~(reg_controllable_hmaster1) ) ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) )) );

// Master 2:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=1)) <-> (X(hmaster0=0) * X(hmaster1=1)) ) );
assign sys_safe_err14 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & reg_controllable_hmaster1 ) ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 )) );

// Master 3:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=1)) <-> (X(hmaster0=1) * X(hmaster1=1)) ) );
assign sys_safe_err15 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & reg_controllable_hmaster1 ) ^~ ( controllable_hmaster0 & controllable_hmaster1 )) );

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

// default master
// G((decide=1  *  hbusreq0=0  *  hbusreq1=0  *  hbusreq2=0  *  hbusreq3=0) -> X(hgrant0=1));
assign sys_safe_err33 =  ~( ~(~reg_controllable_ndecide & (~reg_i_hbusreq0 & ~reg_i_hbusreq1 & ~reg_i_hbusreq2 & ~reg_i_hbusreq3)) | (~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;

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

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


// =============================================================
//                          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))  |  hbusreq0=0));
assign sys_fair2 =  ( ~(controllable_hmaster0) & ~(controllable_hmaster1) ) | ~i_hbusreq0;

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

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

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

assign fair_err = (fair_cnt >= 3'b111);

// 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_controllable_hmaster0 = 0;
  reg_controllable_hmaster1 = 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_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;
  env_safe_err_happened = 0;
  next_env_fair = 0;
  fair_cnt = 0;
  next_sys_fair = 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((next_sys_fair == 0) & sys_fair0)
    begin
      next_sys_fair = 1;
      next_env_fair = 0;
      fair_cnt = 0;
    end
   else if((next_sys_fair == 1) & sys_fair1)
    begin
      next_sys_fair = 2;
      next_env_fair = 0;
      fair_cnt = 0;
    end
   else if((next_sys_fair == 2) & sys_fair2)
    begin
      next_sys_fair = 3;
      next_env_fair = 0;
      fair_cnt = 0;
    end
   else if((next_sys_fair == 3) & sys_fair3)
    begin
      next_sys_fair = 4;
      next_env_fair = 0;
      fair_cnt = 0;
    end
   else if((next_sys_fair == 4) & sys_fair4)
    begin
      next_sys_fair = 5;
      next_env_fair = 0;
      fair_cnt = 0;
    end
   else if((next_sys_fair == 5) & sys_fair5)
    begin
      next_sys_fair = 0;
      next_env_fair = 0;
      fair_cnt = 0;
    end
   else if(~next_env_fair & env_fair0)
    begin
      next_env_fair = 1;
    end
   else if(next_env_fair & env_fair1)
    begin
      next_env_fair = 0;
      fair_cnt = fair_cnt + 1;
    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

   // 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_controllable_hmaster0 =  controllable_hmaster0;
   reg_controllable_hmaster1 =  controllable_hmaster1;
   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_busreq =  controllable_busreq;

 end
endmodule

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