amba3c4unrealn.aag

aag 526 19 34 1 473
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40 1
42 30
44 16
46 653
48 737
50 18
52 761
54 36
56 781
58 2
60 28
62 10
64 4
66 811
68 833
70 38
72 32
74 855
76 879
78 8
80 6
82 935
84 941
86 947
88 953
90 26
92 1041
94 1047
96 1053
98 123
100 22
102 34
104 24
106 20
516
108 22 3
110 26 5
112 111 109
114 32 7
116 115 112
118 99 40
120 119 40
122 121 116
124 21 17
126 29 2
128 28 3
130 129 127
132 131 124
134 20 17
136 29 4
138 28 5
140 139 137
142 141 134
144 143 133
146 21 16
148 29 6
150 28 7
152 151 149
154 153 146
156 155 144
158 103 40
160 102 40
162 159 40
164 163 11
166 165 156
168 67 40
170 66 40
172 169 40
174 170 11
176 175 166
178 49 40
180 48 40
182 179 40
184 53 40
186 52 40
188 185 40
190 189 183
192 57 40
194 56 40
196 193 40
198 197 190
200 199 11
202 201 176
204 71 40
206 70 40
208 205 40
210 206 124
212 209 125
214 213 211
216 215 160
218 217 202
220 105 40
222 104 40
224 221 40
226 225 134
228 222 135
230 229 227
232 231 160
234 233 218
236 43 40
238 42 40
240 237 40
242 241 146
244 238 147
246 245 243
248 247 160
250 249 234
252 51 40
254 50 40
256 253 40
258 254 9
260 257 8
262 261 259
264 263 160
266 265 250
268 107 40
270 106 40
272 269 40
274 45 40
276 44 40
278 275 40
280 279 273
282 281 124
284 280 125
286 285 283
288 287 10
290 289 266
292 279 270
294 293 134
296 292 135
298 297 295
300 299 10
302 301 290
304 276 273
306 305 146
308 304 147
310 309 307
312 311 10
314 313 302
316 79 40
318 78 40
320 317 40
322 321 8
324 318 9
326 325 323
328 327 10
330 329 314
332 55 40
334 54 40
336 333 40
338 101 40
340 100 40
342 339 40
344 340 337
346 344 39
348 346 19
350 349 330
352 343 337
354 352 39
356 354 18
358 357 350
360 91 40
362 90 40
364 361 40
366 362 337
368 366 24
370 368 19
372 371 358
374 365 337
376 374 24
378 376 18
380 379 372
382 73 40
384 72 40
386 383 40
388 384 337
390 388 30
392 390 19
394 393 380
396 387 337
398 396 30
400 398 18
402 401 394
404 209 38
406 206 39
408 407 405
410 409 334
412 411 402
414 222 25
416 225 24
418 417 415
420 419 334
422 421 412
424 238 31
426 241 30
428 427 425
430 429 334
432 431 422
434 254 19
436 257 18
438 437 435
440 439 334
442 441 432
444 69 40
446 68 40
448 445 40
450 24 5
452 450 446
454 453 442
456 75 40
458 74 40
460 457 40
462 30 7
464 462 458
466 465 454
468 59 40
470 469 40
472 65 40
474 473 40
476 475 471
478 81 40
480 479 40
482 481 476
484 482 337
486 484 38
488 487 466
490 97 40
492 96 40
494 491 40
496 95 40
498 94 40
500 497 40
502 93 40
504 92 40
506 503 40
508 505 499
510 508 494
512 511 495
514 512 488
516 515 122
518 83 40
520 82 40
522 519 40
524 85 40
526 84 40
528 525 40
530 87 40
532 86 40
534 531 40
536 88 40
538 527 521
540 538 533
542 540 537
544 542 173
546 527 522
548 546 533
550 548 537
552 550 198
554 528 521
556 554 533
558 556 537
560 125 2
562 561 558
564 528 522
566 564 533
568 566 537
570 135 4
572 571 568
574 538 534
576 574 537
578 147 6
580 579 576
582 47 40
584 46 40
586 583 40
588 77 40
590 76 40
592 589 40
594 593 587
596 584 34
598 552 545
600 599 545
602 553 545
604 602 562
606 605 600
608 602 563
610 608 572
612 611 606
614 608 573
616 614 580
618 617 612
620 614 581
622 620 594
624 623 618
626 620 595
628 626 596
630 629 624
632 597 584
634 632 595
636 635 595
638 637 581
640 638 573
642 640 563
644 642 553
646 644 545
648 646 631
650 630 584
652 651 649
654 198 8
656 654 11
658 656 15
660 658 12
662 660 35
664 660 34
666 189 180
668 666 197
670 668 34
672 186 183
674 672 197
676 674 34
678 186 180
680 678 197
682 680 34
684 194 190
686 684 34
688 664 663
690 689 663
692 665 663
694 692 670
696 695 690
698 692 671
700 698 676
702 701 696
704 698 677
706 704 682
708 707 702
710 704 683
712 710 686
714 713 708
716 687 180
718 716 683
720 718 677
722 721 677
724 723 671
726 724 665
728 726 663
730 729 663
732 731 715
734 714 180
736 735 733
738 687 186
740 738 683
742 740 677
744 743 677
746 745 671
748 747 671
750 749 665
752 751 665
754 753 663
756 754 715
758 714 186
760 759 757
762 687 194
764 762 683
766 765 683
768 767 677
770 768 671
772 770 665
774 772 663
776 774 715
778 714 194
780 779 777
782 11 8
784 782 15
786 784 13
788 786 173
790 170 29
792 791 789
794 787 170
796 795 787
798 170 28
800 797 173
802 798 170
804 803 801
806 805 793
808 792 170
810 809 807
812 449 25
814 812 5
816 446 4
818 816 815
820 819 815
822 817 446
824 822 815
826 825 815
828 827 821
830 820 446
832 831 829
834 461 31
836 834 7
838 458 6
840 838 837
842 841 837
844 839 458
846 844 837
848 847 837
850 849 843
852 842 458
854 853 851
856 593 8
858 856 15
860 858 13
862 590 29
864 862 861
866 865 861
868 863 590
870 868 861
872 871 861
874 873 867
876 866 590
878 877 875
880 581 520
882 880 573
884 882 563
886 885 563
888 887 553
890 888 545
892 891 545
894 581 526
896 894 573
898 896 563
900 899 563
902 901 553
904 903 553
906 905 545
908 581 532
910 908 573
912 911 573
914 913 563
916 914 553
918 916 545
920 581 536
922 920 573
924 922 563
926 924 553
928 926 545
930 893 619
932 618 520
934 933 931
936 906 619
938 618 526
940 939 937
942 918 619
944 618 532
946 945 943
948 928 619
950 618 536
952 951 949
954 629 618
956 596 507
958 597 504
960 959 957
962 594 504
964 961 595
966 965 963
968 967 581
970 968 573
972 970 563
974 972 553
976 974 545
978 504 501
980 505 498
982 981 979
984 983 596
986 597 498
988 987 985
990 594 498
992 989 595
994 993 991
996 995 581
998 996 573
1000 998 563
1002 1000 553
1004 1002 545
1006 504 498
1008 1006 495
1010 1007 492
1012 1011 1009
1014 1013 596
1016 597 492
1018 1017 1015
1020 594 492
1022 1019 595
1024 1023 1021
1026 1025 581
1028 1026 573
1030 1028 563
1032 1030 553
1034 1032 545
1036 976 955
1038 954 504
1040 1039 1037
1042 1004 955
1044 954 498
1046 1045 1043
1048 1034 955
1050 954 492
1052 1051 1049
i0 i_hbusreq0
i1 i_hbusreq1
i2 i_hbusreq2
i3 controllable_hmastlock
i4 controllable_nstart
i5 i_hburst1
i6 i_hburst0
i7 controllable_hmaster1
i8 controllable_locked
i9 controllable_hmaster0
i10 i_hlock0
i11 controllable_hgrant1
i12 i_hlock1
i13 controllable_busreq
i14 controllable_hgrant2
i15 i_hlock2
i16 i_hready
i17 controllable_ndecide
i18 controllable_nhgrant0
l0 n41
l1 reg_controllable_hgrant2_out
l2 reg_controllable_hmaster1_out
l3 next_env_fair_out
l4 reg_stateG3_0_out
l5 reg_controllable_locked_out
l6 reg_stateG3_1_out
l7 reg_controllable_ndecide_out
l8 reg_stateG3_2_out
l9 reg_i_hbusreq0_out
l10 reg_controllable_busreq_out
l11 reg_controllable_nstart_out
l12 reg_i_hbusreq1_out
l13 reg_stateG2_out
l14 reg_stateG10_1_out
l15 reg_controllable_nhgrant0_out
l16 reg_i_hlock2_out
l17 reg_stateG10_2_out
l18 reg_stateA1_out
l19 reg_controllable_hmastlock_out
l20 reg_i_hbusreq2_out
l21 next_sys_fair<0>_out
l22 next_sys_fair<1>_out
l23 next_sys_fair<2>_out
l24 next_sys_fair<3>_out
l25 reg_i_hlock1_out
l26 fair_cnt<0>_out
l27 fair_cnt<1>_out
l28 fair_cnt<2>_out
l29 env_safe_err_happened_out
l30 reg_i_hlock0_out
l31 reg_i_hready_out
l32 reg_controllable_hgrant1_out
l33 reg_controllable_hmaster0_out
o0 o_err
c
amba_3_new_4
This file was written by ABC on Sat Aug 31 20:25:07 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 amba3c4unreal.v   ---gives--> amba3c4unreal.mv
> abc -c "read_blif_mv amba3c4unreal.mv; write_aiger -s amba3c4unrealn.aig"   ---gives--> amba3c4unrealn.aig
> aigtoaig amba3c4unrealn.aig amba3c4unrealn.aag   ---gives--> amba3c4unrealn.aag (this file)
Content of amba3c4unreal.v:
module amba_3_new_4(
        o_err,
        i_clk,
        i_hready,
        i_hbusreq0,
        i_hlock0,
        i_hbusreq1,
        i_hlock1,
        i_hbusreq2,
        i_hlock2,
        i_hburst0,
        i_hburst1,
        controllable_hmaster0,
        controllable_hmaster1,
        controllable_hmastlock,
        controllable_nstart,
        controllable_ndecide,
        controllable_locked,
        controllable_nhgrant0,
        controllable_hgrant1,
        controllable_hgrant2,
        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_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_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_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_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 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_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_err;

wire env_fair0;
wire env_fair1;

wire sys_fair0;
wire sys_fair1;
wire sys_fair2;
wire sys_fair3;
wire sys_fair4;
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);

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

// =============================================================
//                        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)));

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

// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err4 =  ~( ~(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_err5 =  (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_err6 =  ~( ~(reg_i_hready) | ( ~reg_controllable_nhgrant0 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) ) ) );

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

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

// HMASTLOCK:
// G(  (hready=1) -> (locked=0 <-> X(hmastlock=0) ) );
assign sys_safe_err9 =  ~( ~(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_err10 =  ~( ~(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_err11 =  ~( ~(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_err12 =  ~( ~(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_err13 =  ~( ~(controllable_nstart) | ( reg_controllable_hmastlock ^~ controllable_hmastlock) );

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

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

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

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

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

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

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

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

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

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

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

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

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

// =============================================================
//                          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;

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_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_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;
  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 = 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

   // 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_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_busreq =  controllable_busreq;

 end
endmodule

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