amba6f20unrealy.aag

aag 472 29 54 1 389
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 774
64 10
66 54
68 14
70 52
72 18
74 797
76 812
78 814
80 22
82 833
84 834
86 6
88 46
90 28
92 836
94 843
96 30
98 26
100 8
102 38
104 24
106 844
108 846
110 855
112 858
114 40
116 20
118 58
120 862
122 2
124 864
126 42
128 875
130 16
132 884
134 894
136 906
138 918
140 928
142 930
144 934
146 44
148 12
150 32
152 193
154 938
156 48
158 940
160 4
162 944
164 50
166 56
714
168 39 12
170 41 16
172 171 169
174 43 20
176 175 172
178 45 24
180 179 176
182 49 26
184 183 180
186 51 28
188 187 184
190 152 60
192 191 188
194 57 55
196 194 53
198 166 60
200 66 60
202 201 199
204 70 60
206 205 202
208 207 196
210 206 197
212 211 209
214 213 8
216 56 55
218 216 52
220 50 31
222 51 30
224 223 221
226 225 218
228 194 52
230 48 31
232 49 30
234 233 231
236 235 228
238 56 54
240 238 53
242 44 31
244 45 30
246 245 243
248 247 240
250 57 54
252 250 53
254 42 31
256 43 30
258 257 255
260 259 252
262 38 31
264 39 30
266 265 263
268 267 196
270 216 53
272 40 31
274 41 30
276 275 273
278 277 270
280 74 60
282 82 60
284 283 281
286 94 60
288 287 284
290 110 60
292 150 60
294 292 291
296 294 288
298 297 9
300 86 60
302 300 59
304 301 58
306 305 303
308 80 60
310 309 218
312 308 219
314 313 311
316 72 60
318 317 228
320 316 229
322 321 319
324 68 60
326 325 240
328 324 241
330 329 327
332 64 60
334 333 252
336 332 253
338 337 335
340 122 60
342 340 196
344 341 197
346 345 343
348 160 60
350 349 270
352 348 271
354 353 351
356 354 346
358 356 338
360 358 330
362 360 322
364 362 314
366 364 306
368 367 292
370 369 299
372 370 279
374 372 269
376 374 261
378 376 249
380 378 237
382 380 227
384 382 215
386 201 198
388 386 205
390 389 270
392 388 271
394 393 391
396 395 8
398 397 384
400 200 199
402 400 205
404 403 252
406 402 253
408 407 405
410 409 8
412 411 398
414 200 198
416 414 205
418 417 240
420 416 241
422 421 419
424 423 8
426 425 412
428 204 202
430 429 228
432 428 229
434 433 431
436 435 8
438 437 426
440 386 204
442 441 218
444 440 219
446 445 443
448 447 8
450 449 438
452 118 60
454 453 58
456 452 59
458 457 455
460 459 8
462 461 450
464 148 60
466 88 60
468 467 464
470 468 3
472 470 7
474 473 462
476 467 465
478 476 3
480 478 6
482 481 474
484 130 60
486 484 467
488 486 4
490 488 7
492 491 482
494 485 467
496 494 4
498 496 6
500 499 492
502 116 60
504 502 467
506 504 10
508 506 7
510 509 500
512 503 467
514 512 10
516 514 6
518 517 510
520 104 60
522 520 467
524 522 14
526 524 7
528 527 518
530 521 467
532 530 14
534 532 6
536 535 528
538 98 60
540 538 467
542 540 18
544 542 7
546 545 536
548 539 467
550 548 18
552 550 6
554 553 546
556 90 60
558 556 467
560 558 22
562 560 7
564 563 554
566 557 467
568 566 22
570 568 6
572 571 564
574 341 2
576 340 3
578 577 575
580 579 466
582 581 572
584 348 5
586 349 4
588 587 585
590 589 466
592 591 582
594 332 11
596 333 10
598 597 595
600 599 466
602 601 592
604 324 15
606 325 14
608 607 605
610 609 466
612 611 602
614 316 19
616 317 18
618 617 615
620 619 466
622 621 612
624 308 23
626 309 22
628 627 625
630 629 466
632 631 622
634 300 7
636 301 6
638 637 635
640 639 466
642 641 632
644 112 60
646 41 4
648 646 644
650 649 642
652 120 60
654 43 10
656 654 652
658 657 650
660 144 60
662 45 14
664 662 660
666 665 658
668 154 60
670 49 18
672 670 668
674 673 666
676 162 60
678 51 22
680 678 676
682 681 674
684 115 103
686 684 165
688 147 127
690 688 157
692 690 686
694 693 60
696 695 467
698 696 2
700 699 682
702 138 60
704 136 60
706 705 703
708 140 60
710 708 707
712 711 700
714 713 192
716 241 44
718 62 60
720 719 716
722 78 60
724 723 290
726 106 60
728 727 289
730 729 725
732 197 38
734 158 60
736 735 732
738 737 730
740 271 40
742 84 60
744 743 740
746 745 738
748 253 42
750 124 60
752 751 748
754 753 746
756 754 721
758 229 48
760 92 60
762 761 758
764 763 756
766 219 50
768 142 60
770 769 766
772 771 764
774 773 721
776 58 9
778 776 37
780 778 288
782 780 34
784 782 33
786 287 32
788 787 281
790 786 280
792 791 789
794 792 285
796 795 785
798 76 60
800 799 33
802 128 60
804 108 60
806 805 802
808 807 801
810 809 773
812 810 801
814 773 725
816 782 32
818 282 280
820 818 287
822 820 32
824 823 282
826 283 280
828 826 786
830 829 825
832 830 817
834 773 745
836 773 763
838 284 32
840 839 286
842 841 823
844 773 729
846 810 807
848 290 30
850 291 35
852 850 778
854 853 849
856 645 4
858 857 41
860 653 10
862 861 43
864 773 753
866 803 58
868 37 35
870 868 866
872 802 30
874 873 871
876 132 60
878 876 808
880 877 809
882 881 879
884 882 773
886 134 60
888 886 879
890 887 878
892 891 889
894 893 773
896 886 876
898 896 808
900 899 704
902 898 705
904 903 901
906 905 773
908 896 704
910 908 808
912 911 702
914 910 703
916 915 913
918 917 773
920 910 702
922 921 709
924 920 708
926 925 923
928 926 773
930 773 771
932 661 14
934 933 45
936 669 18
938 937 49
940 773 737
942 677 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 fair_cnt<3>_out
l40 fair_cnt<4>_out
l41 sys_fair7done_out
l42 reg_stateG10_3_out
l43 reg_i_hbusreq3_out
l44 reg_i_hlock0_out
l45 reg_i_hready_out
l46 env_safe_err_happened_out
l47 reg_stateG10_4_out
l48 reg_i_hbusreq4_out
l49 sys_fair2done_out
l50 reg_controllable_hgrant1_out
l51 reg_stateG10_5_out
l52 reg_i_hbusreq5_out
l53 reg_controllable_hmaster0_out
o0 o_err
c
amba_6_new_20
This file was written by ABC on Sat Aug 31 20:25:04 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 amba6f20unreal.v   ---gives--> amba6f20unreal.mv
> abc -c "read_blif_mv amba6f20unreal.mv; strash; refactor; rewrite; dfraig; rewrite; dfraig; write_aiger -s amba6f20unrealy.aig"   ---gives--> amba6f20unrealy.aig
> aigtoaig amba6f20unrealy.aig amba6f20unrealy.aag   ---gives--> amba6f20unrealy.aag (this file)
Content of amba6f20unreal.v:
module amba_6_new_20(
        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 [4: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 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 fair_err = (fair_cnt >= 5'b10100);

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

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

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