amba6b5y.aag

aag 472 29 52 1 391
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 1
62 770
64 10
66 54
68 14
70 52
72 18
74 793
76 840
78 842
80 22
82 861
84 862
86 6
88 46
90 28
92 864
94 871
96 30
98 26
100 8
102 38
104 24
106 872
108 874
110 883
112 886
114 40
116 20
118 58
120 890
122 2
124 892
126 42
128 903
130 16
132 910
134 918
136 928
138 930
140 934
142 44
144 12
146 32
148 189
150 938
152 48
154 940
156 4
158 944
160 50
162 56
710
164 39 12
166 41 16
168 167 165
170 43 20
172 171 168
174 45 24
176 175 172
178 49 26
180 179 176
182 51 28
184 183 180
186 148 60
188 187 184
190 57 55
192 190 53
194 162 60
196 66 60
198 197 195
200 70 60
202 201 198
204 203 192
206 202 193
208 207 205
210 209 8
212 56 55
214 212 52
216 50 31
218 51 30
220 219 217
222 221 214
224 190 52
226 48 31
228 49 30
230 229 227
232 231 224
234 56 54
236 234 53
238 44 31
240 45 30
242 241 239
244 243 236
246 57 54
248 246 53
250 42 31
252 43 30
254 253 251
256 255 248
258 38 31
260 39 30
262 261 259
264 263 192
266 212 53
268 40 31
270 41 30
272 271 269
274 273 266
276 74 60
278 82 60
280 279 277
282 94 60
284 283 280
286 110 60
288 146 60
290 288 287
292 290 284
294 293 9
296 86 60
298 296 59
300 297 58
302 301 299
304 80 60
306 305 214
308 304 215
310 309 307
312 72 60
314 313 224
316 312 225
318 317 315
320 68 60
322 321 236
324 320 237
326 325 323
328 64 60
330 329 248
332 328 249
334 333 331
336 122 60
338 336 192
340 337 193
342 341 339
344 156 60
346 345 266
348 344 267
350 349 347
352 350 342
354 352 334
356 354 326
358 356 318
360 358 310
362 360 302
364 363 288
366 365 295
368 366 275
370 368 265
372 370 257
374 372 245
376 374 233
378 376 223
380 378 211
382 197 194
384 382 201
386 385 266
388 384 267
390 389 387
392 391 8
394 393 380
396 196 195
398 396 201
400 399 248
402 398 249
404 403 401
406 405 8
408 407 394
410 196 194
412 410 201
414 413 236
416 412 237
418 417 415
420 419 8
422 421 408
424 200 198
426 425 224
428 424 225
430 429 427
432 431 8
434 433 422
436 382 200
438 437 214
440 436 215
442 441 439
444 443 8
446 445 434
448 118 60
450 449 58
452 448 59
454 453 451
456 455 8
458 457 446
460 144 60
462 88 60
464 463 460
466 464 3
468 466 7
470 469 458
472 463 461
474 472 3
476 474 6
478 477 470
480 130 60
482 480 463
484 482 4
486 484 7
488 487 478
490 481 463
492 490 4
494 492 6
496 495 488
498 116 60
500 498 463
502 500 10
504 502 7
506 505 496
508 499 463
510 508 10
512 510 6
514 513 506
516 104 60
518 516 463
520 518 14
522 520 7
524 523 514
526 517 463
528 526 14
530 528 6
532 531 524
534 98 60
536 534 463
538 536 18
540 538 7
542 541 532
544 535 463
546 544 18
548 546 6
550 549 542
552 90 60
554 552 463
556 554 22
558 556 7
560 559 550
562 553 463
564 562 22
566 564 6
568 567 560
570 337 2
572 336 3
574 573 571
576 575 462
578 577 568
580 344 5
582 345 4
584 583 581
586 585 462
588 587 578
590 328 11
592 329 10
594 593 591
596 595 462
598 597 588
600 320 15
602 321 14
604 603 601
606 605 462
608 607 598
610 312 19
612 313 18
614 613 611
616 615 462
618 617 608
620 304 23
622 305 22
624 623 621
626 625 462
628 627 618
630 296 7
632 297 6
634 633 631
636 635 462
638 637 628
640 112 60
642 41 4
644 642 640
646 645 638
648 120 60
650 43 10
652 650 648
654 653 646
656 140 60
658 45 14
660 658 656
662 661 654
664 150 60
666 49 18
668 666 664
670 669 662
672 158 60
674 51 22
676 674 672
678 677 670
680 115 103
682 680 161
684 143 127
686 684 153
688 686 682
690 689 60
692 691 463
694 692 2
696 695 678
698 134 60
700 132 60
702 701 699
704 136 60
706 704 703
708 707 696
710 709 188
712 237 44
714 62 60
716 715 712
718 78 60
720 719 286
722 106 60
724 723 285
726 725 721
728 193 38
730 154 60
732 731 728
734 733 726
736 267 40
738 84 60
740 739 736
742 741 734
744 249 42
746 124 60
748 747 744
750 749 742
752 750 717
754 225 48
756 92 60
758 757 754
760 759 752
762 215 50
764 138 60
766 765 762
768 767 760
770 769 717
772 58 9
774 772 37
776 774 284
778 776 34
780 778 33
782 283 32
784 783 277
786 782 276
788 787 785
790 788 281
792 791 781
794 76 60
796 795 33
798 128 60
800 108 60
802 801 798
804 803 797
806 719 287
808 723 284
810 809 807
812 731 729
814 813 810
816 739 737
818 817 814
820 747 745
822 821 818
824 715 713
826 825 822
828 757 755
830 829 826
832 765 763
834 833 830
836 834 769
838 836 805
840 838 797
842 769 721
844 778 32
846 278 276
848 846 283
850 848 32
852 851 278
854 279 276
856 854 782
858 857 853
860 858 845
862 769 741
864 769 759
866 280 32
868 867 282
870 869 851
872 769 725
874 838 803
876 286 30
878 287 35
880 878 774
882 881 877
884 641 4
886 885 41
888 649 10
890 889 43
892 769 749
894 799 58
896 37 35
898 896 894
900 798 30
902 901 899
904 804 700
906 805 701
908 907 905
910 908 836
912 905 698
914 904 699
916 915 913
918 917 836
920 904 698
922 921 705
924 920 704
926 925 923
928 926 836
930 769 767
932 657 14
934 933 45
936 665 18
938 937 49
940 769 733
942 673 22
944 943 51
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 i_hlock4
i13 i_hlock5
i14 controllable_busreq
i15 i_hready
i16 i_hburst1
i17 i_hburst0
i18 i_hbusreq0
i19 i_hbusreq1
i20 i_hbusreq2
i21 i_hbusreq3
i22 controllable_ndecide
i23 i_hbusreq4
i24 i_hbusreq5
i25 controllable_hmaster2
i26 controllable_hmaster1
i27 controllable_hmaster0
i28 controllable_hmastlock
l0 n61
l1 sys_fair5done_out
l2 reg_controllable_hgrant2_out
l3 reg_controllable_hmaster1_out
l4 reg_controllable_hgrant3_out
l5 reg_controllable_hmaster2_out
l6 reg_controllable_hgrant4_out
l7 reg_stateG3_0_out
l8 env_fair1done_out
l9 sys_fair0done_out
l10 reg_controllable_hgrant5_out
l11 reg_stateG3_1_out
l12 sys_fair3done_out
l13 reg_controllable_locked_out
l14 reg_controllable_ndecide_out
l15 reg_i_hlock5_out
l16 sys_fair6done_out
l17 reg_stateG3_2_out
l18 reg_controllable_busreq_out
l19 reg_i_hlock4_out
l20 reg_controllable_nstart_out
l21 reg_i_hbusreq0_out
l22 reg_i_hlock3_out
l23 sys_fair1done_out
l24 env_fair0done_out
l25 reg_stateG2_out
l26 reg_stateG10_1_out
l27 reg_i_hbusreq1_out
l28 reg_i_hlock2_out
l29 reg_controllable_hmastlock_out
l30 reg_stateG10_2_out
l31 reg_controllable_nhgrant0_out
l32 sys_fair4done_out
l33 reg_i_hbusreq2_out
l34 reg_stateA1_out
l35 reg_i_hlock1_out
l36 fair_cnt<0>_out
l37 fair_cnt<1>_out
l38 fair_cnt<2>_out
l39 sys_fair7done_out
l40 reg_stateG10_3_out
l41 reg_i_hbusreq3_out
l42 reg_i_hlock0_out
l43 reg_i_hready_out
l44 env_safe_err_happened_out
l45 reg_stateG10_4_out
l46 reg_i_hbusreq4_out
l47 sys_fair2done_out
l48 reg_controllable_hgrant1_out
l49 reg_stateG10_5_out
l50 reg_i_hbusreq5_out
l51 reg_controllable_hmaster0_out
o0 o_err
c
amba_6_new_5
This file was written by ABC on Sat Aug 31 20:24:57 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 amba6b5.v   ---gives--> amba6b5.mv
> abc -c "read_blif_mv amba6b5.mv; strash; refactor; rewrite; dfraig; rewrite; dfraig; write_aiger -s amba6b5y.aig"   ---gives--> amba6b5y.aig
> aigtoaig amba6b5y.aig amba6b5y.aag   ---gives--> amba6b5y.aag (this file)
Content of amba6b5.v:
module amba_6_new_5(
        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_hburst0,
        i_hburst1,
        controllable_hmaster0,
        controllable_hmaster1,
        controllable_hmaster2,
        controllable_hmastlock,
        controllable_nstart,
        controllable_ndecide,
        controllable_locked,
        controllable_nhgrant0,
        controllable_hgrant1,
        controllable_hgrant2,
        controllable_hgrant3,
        controllable_hgrant4,
        controllable_hgrant5,
        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_hburst0;
input i_hburst1;
input controllable_hmaster0;
input controllable_hmaster1;
input controllable_hmaster2;
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_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_controllable_hmaster0;
reg reg_controllable_hmaster1;
reg reg_controllable_hmaster2;
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_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 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 [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_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_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 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);

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

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

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

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

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

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

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

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

// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err7 =  ~( ~(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_err8 =  (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))  ) );
assign sys_safe_err9 =  ~( ~(reg_i_hready) | ( ~reg_controllable_nhgrant0 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & ~(controllable_hmaster2) ) ) );

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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);
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);
assign fair_err = (fair_cnt >= 3'b101);

// 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_controllable_hmaster0 = 0;
  reg_controllable_hmaster1 = 0;
  reg_controllable_hmaster2 = 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_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;
  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;
  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;
      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;
       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

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

 end
endmodule

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