-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathamba4f25n.aag
executable file
·1229 lines (1159 loc) · 27.3 KB
/
amba4f25n.aag
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
aag 576 22 43 1 511
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46 1
48 32
50 18
52 742
54 36
56 744
58 829
60 871
62 20
64 872
66 897
68 42
70 917
72 2
74 30
76 12
78 4
80 38
82 918
84 949
86 971
88 981
90 44
92 34
94 1003
96 1027
98 8
100 1028
102 6
104 28
106 1051
108 1127
110 1133
112 1139
114 1145
116 1151
118 10
120 151
122 24
124 40
126 26
128 22
130 1152
686
132 24 3
134 28 5
136 135 133
138 34 7
140 139 136
142 38 11
144 143 140
146 121 46
148 147 46
150 149 144
152 23 19
154 31 2
156 30 3
158 157 155
160 159 152
162 22 19
164 31 4
166 30 5
168 167 165
170 169 162
172 171 161
174 23 18
176 31 6
178 30 7
180 179 177
182 181 174
184 183 172
186 22 18
188 31 10
190 30 11
192 191 189
194 193 186
196 195 184
198 125 46
200 124 46
202 199 46
204 203 13
206 205 196
208 85 46
210 84 46
212 209 46
214 210 13
216 215 206
218 59 46
220 58 46
222 219 46
224 67 46
226 66 46
228 225 46
230 229 223
232 71 46
234 70 46
236 233 46
238 237 230
240 239 13
242 241 216
244 91 46
246 90 46
248 245 46
250 246 152
252 249 153
254 253 251
256 255 200
258 257 242
260 127 46
262 126 46
264 261 46
266 265 162
268 262 163
270 269 267
272 271 200
274 273 258
276 49 46
278 48 46
280 277 46
282 281 174
284 278 175
286 285 283
288 287 200
290 289 274
292 55 46
294 54 46
296 293 46
298 297 186
300 294 187
302 301 299
304 303 200
306 305 290
308 63 46
310 62 46
312 309 46
314 310 9
316 313 8
318 317 315
320 319 200
322 321 306
324 129 46
326 128 46
328 325 46
330 51 46
332 50 46
334 331 46
336 335 329
338 337 152
340 336 153
342 341 339
344 343 12
346 345 322
348 335 326
350 349 162
352 348 163
354 353 351
356 355 12
358 357 346
360 332 329
362 361 174
364 360 175
366 365 363
368 367 12
370 369 358
372 332 326
374 373 186
376 372 187
378 377 375
380 379 12
382 381 370
384 99 46
386 98 46
388 385 46
390 389 8
392 386 9
394 393 391
396 395 12
398 397 382
400 69 46
402 68 46
404 401 46
406 123 46
408 122 46
410 407 46
412 408 405
414 412 45
416 414 21
418 417 398
420 411 405
422 420 45
424 422 20
426 425 418
428 105 46
430 104 46
432 429 46
434 430 405
436 434 26
438 436 21
440 439 426
442 433 405
444 442 26
446 444 20
448 447 440
450 93 46
452 92 46
454 451 46
456 452 405
458 456 32
460 458 21
462 461 448
464 455 405
466 464 32
468 466 20
470 469 462
472 81 46
474 80 46
476 473 46
478 474 405
480 478 36
482 480 21
484 483 470
486 477 405
488 486 36
490 488 20
492 491 484
494 249 44
496 246 45
498 497 495
500 499 402
502 501 492
504 262 27
506 265 26
508 507 505
510 509 402
512 511 502
514 278 33
516 281 32
518 517 515
520 519 402
522 521 512
524 294 37
526 297 36
528 527 525
530 529 402
532 531 522
534 310 21
536 313 20
538 537 535
540 539 402
542 541 532
544 87 46
546 86 46
548 545 46
550 26 5
552 550 546
554 553 542
556 95 46
558 94 46
560 557 46
562 32 7
564 562 558
566 565 554
568 107 46
570 106 46
572 569 46
574 36 11
576 574 570
578 577 566
580 73 46
582 581 46
584 79 46
586 585 46
588 587 583
590 103 46
592 591 46
594 593 588
596 119 46
598 597 46
600 599 594
602 600 405
604 602 44
606 605 578
608 117 46
610 116 46
612 609 46
614 115 46
616 114 46
618 615 46
620 113 46
622 112 46
624 621 46
626 111 46
628 110 46
630 627 46
632 109 46
634 108 46
636 633 46
638 637 631
640 638 625
642 640 619
644 643 618
646 644 641
648 647 613
650 649 612
652 650 646
654 636 628
656 655 639
658 639 622
660 659 641
662 641 619
664 640 616
666 665 663
668 646 613
670 647 610
672 671 669
674 656 636
676 674 660
678 676 666
680 678 672
682 681 653
684 682 606
686 685 150
688 57 46
690 689 46
692 691 210
694 83 46
696 695 46
698 697 239
700 699 693
702 131 46
704 703 46
706 153 2
708 706 705
710 709 700
712 65 46
714 713 46
716 163 4
718 716 715
720 719 710
722 101 46
724 723 46
726 175 6
728 726 725
730 729 720
732 53 46
734 733 46
736 187 10
738 736 735
740 739 730
742 741 739
744 741 693
746 238 8
748 746 13
750 748 17
752 750 14
754 752 41
756 752 40
758 229 220
760 758 237
762 760 40
764 226 223
766 764 237
768 766 40
770 226 220
772 770 237
774 772 40
776 234 230
778 776 40
780 756 755
782 781 755
784 757 755
786 784 762
788 787 782
790 784 763
792 790 768
794 793 788
796 790 769
798 796 774
800 799 794
802 796 775
804 802 778
806 805 800
808 779 220
810 808 775
812 810 769
814 813 769
816 815 763
818 816 757
820 818 755
822 821 755
824 823 807
826 806 220
828 827 825
830 89 46
832 88 46
834 831 46
836 97 46
838 96 46
840 837 46
842 838 835
844 61 46
846 60 46
848 845 46
850 849 41
852 851 843
854 852 741
856 855 741
858 853 741
860 859 856
862 853 851
864 862 741
866 864 861
868 860 846
870 869 867
872 741 719
874 779 226
876 874 775
878 876 769
880 879 769
882 881 763
884 883 763
886 885 757
888 887 757
890 889 755
892 890 807
894 806 226
896 895 893
898 779 234
900 898 775
902 901 775
904 903 769
906 904 763
908 906 757
910 908 755
912 910 807
914 806 234
916 915 913
918 741 699
920 13 8
922 920 17
924 922 15
926 924 213
928 210 31
930 929 927
932 925 210
934 933 925
936 210 30
938 935 213
940 936 210
942 941 939
944 943 931
946 930 210
948 947 945
950 549 27
952 950 5
954 546 4
956 954 953
958 957 953
960 955 546
962 960 953
964 963 953
966 965 959
968 958 546
970 969 967
972 853 843
974 972 741
976 974 861
978 860 832
980 979 977
982 561 33
984 982 7
986 558 6
988 986 985
990 989 985
992 987 558
994 992 985
996 995 985
998 997 991
1000 990 558
1002 1001 999
1004 841 8
1006 1004 17
1008 1006 15
1010 838 31
1012 1010 1009
1014 1013 1009
1016 1011 838
1018 1016 1009
1020 1019 1009
1022 1021 1015
1024 1014 838
1026 1025 1023
1028 741 729
1030 573 37
1032 1030 11
1034 570 10
1036 1034 1033
1038 1037 1033
1040 1035 570
1042 1040 1033
1044 1043 1033
1046 1045 1039
1048 1038 570
1050 1049 1047
1052 852 637
1054 853 634
1056 1055 1053
1058 1057 741
1060 634 631
1062 635 628
1064 1063 1061
1066 1065 852
1068 853 628
1070 1069 1067
1072 1071 741
1074 634 628
1076 1074 625
1078 1075 622
1080 1079 1077
1082 1081 852
1084 853 622
1086 1085 1083
1088 1087 741
1090 1074 622
1092 1090 619
1094 1091 616
1096 1095 1093
1098 1097 852
1100 853 616
1102 1101 1099
1104 1103 741
1106 1090 616
1108 1106 613
1110 1107 610
1112 1111 1109
1114 1113 852
1116 853 610
1118 1117 1115
1120 1119 741
1122 1058 857
1124 856 634
1126 1125 1123
1128 1072 857
1130 856 628
1132 1131 1129
1134 1088 857
1136 856 622
1138 1137 1135
1140 1104 857
1142 856 616
1144 1143 1141
1146 1120 857
1148 856 610
1150 1149 1147
1152 741 709
i0 i_hbusreq0
i1 i_hbusreq1
i2 i_hbusreq2
i3 controllable_hmastlock
i4 i_hbusreq3
i5 controllable_nstart
i6 i_hburst1
i7 i_hburst0
i8 controllable_hmaster1
i9 controllable_locked
i10 controllable_hmaster0
i11 i_hlock0
i12 controllable_hgrant1
i13 i_hlock1
i14 controllable_busreq
i15 controllable_hgrant2
i16 i_hlock2
i17 controllable_hgrant3
i18 i_hlock3
i19 i_hready
i20 controllable_ndecide
i21 controllable_nhgrant0
l0 n47
l1 reg_controllable_hgrant2_out
l2 reg_controllable_hmaster1_out
l3 sys_fair5done_out
l4 reg_controllable_hgrant3_out
l5 sys_fair0done_out
l6 reg_stateG3_0_out
l7 env_fair1done_out
l8 reg_controllable_locked_out
l9 sys_fair3done_out
l10 reg_stateG3_1_out
l11 reg_controllable_ndecide_out
l12 reg_stateG3_2_out
l13 reg_i_hbusreq0_out
l14 reg_controllable_busreq_out
l15 reg_controllable_nstart_out
l16 reg_i_hbusreq1_out
l17 reg_i_hlock3_out
l18 sys_fair1done_out
l19 reg_stateG2_out
l20 reg_stateG10_1_out
l21 env_fair0done_out
l22 reg_controllable_nhgrant0_out
l23 reg_i_hlock2_out
l24 reg_stateG10_2_out
l25 reg_stateA1_out
l26 reg_controllable_hmastlock_out
l27 sys_fair4done_out
l28 reg_i_hbusreq2_out
l29 reg_i_hlock1_out
l30 reg_stateG10_3_out
l31 fair_cnt<0>_out
l32 fair_cnt<1>_out
l33 fair_cnt<2>_out
l34 fair_cnt<3>_out
l35 fair_cnt<4>_out
l36 reg_i_hbusreq3_out
l37 env_safe_err_happened_out
l38 reg_i_hlock0_out
l39 reg_i_hready_out
l40 reg_controllable_hgrant1_out
l41 reg_controllable_hmaster0_out
l42 sys_fair2done_out
o0 o_err
c
amba_4_new_25
This file was written by ABC on Sat Aug 31 20:24:56 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 amba4f25.v ---gives--> amba4f25.mv
> abc -c "read_blif_mv amba4f25.mv; write_aiger -s amba4f25n.aig" ---gives--> amba4f25n.aig
> aigtoaig amba4f25n.aig amba4f25n.aag ---gives--> amba4f25n.aag (this file)
Content of amba4f25.v:
module amba_4_new_25(
o_err,
i_clk,
i_hready,
i_hbusreq0,
i_hlock0,
i_hbusreq1,
i_hlock1,
i_hbusreq2,
i_hlock2,
i_hbusreq3,
i_hlock3,
i_hburst0,
i_hburst1,
controllable_hmaster0,
controllable_hmaster1,
controllable_hmastlock,
controllable_nstart,
controllable_ndecide,
controllable_locked,
controllable_nhgrant0,
controllable_hgrant1,
controllable_hgrant2,
controllable_hgrant3,
controllable_busreq);
input i_clk;
input i_hready;
input i_hbusreq0;
input i_hlock0;
input i_hbusreq1;
input i_hlock1;
input i_hbusreq2;
input i_hlock2;
input i_hbusreq3;
input i_hlock3;
input i_hburst0;
input i_hburst1;
input controllable_hmaster0;
input controllable_hmaster1;
input controllable_hmastlock;
input controllable_nstart;
input controllable_ndecide;
input controllable_locked;
input controllable_nhgrant0;
input controllable_hgrant1;
input controllable_hgrant2;
input controllable_hgrant3;
input controllable_busreq;
output o_err;
reg reg_i_hready;
reg reg_i_hbusreq0;
reg reg_i_hlock0;
reg reg_i_hbusreq1;
reg reg_i_hlock1;
reg reg_i_hbusreq2;
reg reg_i_hlock2;
reg reg_i_hbusreq3;
reg reg_i_hlock3;
reg reg_controllable_hmaster0;
reg reg_controllable_hmaster1;
reg reg_controllable_hmastlock;
reg reg_controllable_nstart;
reg reg_controllable_ndecide;
reg reg_controllable_locked;
reg reg_controllable_nhgrant0;
reg reg_controllable_hgrant1;
reg reg_controllable_hgrant2;
reg reg_controllable_hgrant3;
reg reg_controllable_busreq;
reg reg_stateA1;
reg reg_stateG2;
reg reg_stateG3_0;
reg reg_stateG3_1;
reg reg_stateG3_2;
reg reg_stateG10_1;
reg reg_stateG10_2;
reg reg_stateG10_3;
reg env_safe_err_happened;
reg env_fair0done;
reg env_fair1done;
reg sys_fair0done;
reg sys_fair1done;
reg sys_fair2done;
reg sys_fair3done;
reg sys_fair4done;
reg sys_fair5done;
reg [4:0] fair_cnt;
wire env_safe_err0;
wire env_safe_err1;
wire env_safe_err2;
wire env_safe_err3;
wire env_safe_err;
wire sys_safe_err0;
wire sys_safe_err1;
wire sys_safe_err2;
wire sys_safe_err3;
wire sys_safe_err4;
wire sys_safe_err5;
wire sys_safe_err6;
wire sys_safe_err7;
wire sys_safe_err8;
wire sys_safe_err9;
wire sys_safe_err10;
wire sys_safe_err11;
wire sys_safe_err12;
wire sys_safe_err13;
wire sys_safe_err14;
wire sys_safe_err15;
wire sys_safe_err16;
wire sys_safe_err17;
wire sys_safe_err18;
wire sys_safe_err19;
wire sys_safe_err20;
wire sys_safe_err21;
wire sys_safe_err22;
wire sys_safe_err23;
wire sys_safe_err24;
wire sys_safe_err25;
wire sys_safe_err26;
wire sys_safe_err27;
wire sys_safe_err28;
wire sys_safe_err29;
wire sys_safe_err30;
wire sys_safe_err31;
wire sys_safe_err32;
wire sys_safe_err33;
wire sys_safe_err;
wire env_fair0;
wire env_fair1;
wire sys_fair0;
wire sys_fair1;
wire sys_fair2;
wire sys_fair3;
wire sys_fair4;
wire sys_fair5;
wire 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);
// collecting together the safety error bits:
assign env_safe_err = env_safe_err0 |
env_safe_err1 |
env_safe_err2 |
env_safe_err3;
// =============================================================
// SYS_TRANSITION:
// =============================================================
// G((hmaster0=0) * (hmaster1=0) -> (hbusreq0=0 <-> busreq=0));
assign sys_safe_err0 = ~( ~( ~(controllable_hmaster0) & ~(controllable_hmaster1) )|(~i_hbusreq0 ^~ (~controllable_busreq)));
// G((hmaster0=1) * (hmaster1=0) -> (hbusreq1=0 <-> busreq=0));
assign sys_safe_err1 = ~( ~( controllable_hmaster0 & ~(controllable_hmaster1) )|(~i_hbusreq1 ^~ (~controllable_busreq)));
// G((hmaster0=0) * (hmaster1=1) -> (hbusreq2=0 <-> busreq=0));
assign sys_safe_err2 = ~( ~( ~(controllable_hmaster0) & controllable_hmaster1 )|(~i_hbusreq2 ^~ (~controllable_busreq)));
// G((hmaster0=1) * (hmaster1=1) -> (hbusreq3=0 <-> busreq=0));
assign sys_safe_err3 = ~( ~( controllable_hmaster0 & controllable_hmaster1 )|(~i_hbusreq3 ^~ (~controllable_busreq)));
// Guarantee 1:
// G((hready=0) -> X(start=0));
assign sys_safe_err4 = ~( reg_i_hready | controllable_nstart );
// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err5 = ~( ~(reg_stateG2 & ~controllable_nstart) | 0 );
// G(((stateG3_0=1) * (stateG3_1=0) * (stateG3_2=0) * ((start=1))) -> FALSE);
// G(((stateG3_0=0) * (stateG3_1=1) * (stateG3_2=0) * ((start=1))) -> FALSE);
// G(((stateG3_0=1) * (stateG3_1=1) * (stateG3_2=0) * ((start=1))) -> FALSE);
// G(((stateG3_0=0) * (stateG3_1=0) * (stateG3_2=1) * ((start=1))) -> FALSE);
// all these rules can be summarized as: only in state 000, start=1 is allowed:
assign sys_safe_err6 = (reg_stateG3_0 | reg_stateG3_1 | reg_stateG3_2) & ~controllable_nstart;
// G( (hready=1) -> ( (hgrant0=1) <-> (X(hmaster0=0) * X(hmaster1=0)) ) );
assign sys_safe_err7 = ~( ~(reg_i_hready) | ( ~reg_controllable_nhgrant0 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) ) ) );
// G( (hready=1) -> ( (hgrant1=1) <-> (X(hmaster0=1) * X(hmaster1=0)) ) );
assign sys_safe_err8 = ~( ~(reg_i_hready) | ( reg_controllable_hgrant1 ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) ) ) );
// G( (hready=1) -> ( (hgrant2=1) <-> (X(hmaster0=0) * X(hmaster1=1)) ) );
assign sys_safe_err9 = ~( ~(reg_i_hready) | ( reg_controllable_hgrant2 ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 ) ) );
// G( (hready=1) -> ( (hgrant3=1) <-> (X(hmaster0=1) * X(hmaster1=1)) ) );
assign sys_safe_err10 = ~( ~(reg_i_hready) | ( reg_controllable_hgrant3 ^~ ( controllable_hmaster0 & controllable_hmaster1 ) ) );
// HMASTLOCK:
// G( (hready=1) -> (locked=0 <-> X(hmastlock=0) ) );
assign sys_safe_err11 = ~( ~(reg_i_hready) | (~reg_controllable_locked ^~ ~controllable_hmastlock) );
// Master 0:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=0)) <-> (X(hmaster0=0) * X(hmaster1=0)) ) );
assign sys_safe_err12 = ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) )) );
// Master 1:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=0)) <-> (X(hmaster0=1) * X(hmaster1=0)) ) );
assign sys_safe_err13 = ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & ~(reg_controllable_hmaster1) ) ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) )) );
// Master 2:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=1)) <-> (X(hmaster0=0) * X(hmaster1=1)) ) );
assign sys_safe_err14 = ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & reg_controllable_hmaster1 ) ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 )) );
// Master 3:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=1)) <-> (X(hmaster0=1) * X(hmaster1=1)) ) );
assign sys_safe_err15 = ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & reg_controllable_hmaster1 ) ^~ ( controllable_hmaster0 & controllable_hmaster1 )) );
// Guarantee 6.2:
// G( ((X(start=0))) -> ( (hmastlock=1) <-> X(hmastlock=1)) );
assign sys_safe_err16 = ~( ~(controllable_nstart) | ( reg_controllable_hmastlock ^~ controllable_hmastlock) );
// G( (decide=1 * hlock0=1 * X(hgrant0=1) )->X(locked=1));
assign sys_safe_err17 = ~( ~(~reg_controllable_ndecide & reg_i_hlock0 & ~controllable_nhgrant0) | (controllable_locked) );
// G((decide=1 * hlock0=0 * X(hgrant0=1))->X(locked=0));
assign sys_safe_err18 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock0 & ~controllable_nhgrant0) | (~controllable_locked) );
// G( (decide=1 * hlock1=1 * X(hgrant1=1) )->X(locked=1));
assign sys_safe_err19 = ~( ~(~reg_controllable_ndecide & reg_i_hlock1 & controllable_hgrant1) | (controllable_locked) );
// G((decide=1 * hlock1=0 * X(hgrant1=1))->X(locked=0));
assign sys_safe_err20 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock1 & controllable_hgrant1) | (~controllable_locked) );
// G( (decide=1 * hlock2=1 * X(hgrant2=1) )->X(locked=1));
assign sys_safe_err21 = ~( ~(~reg_controllable_ndecide & reg_i_hlock2 & controllable_hgrant2) | (controllable_locked) );
// G((decide=1 * hlock2=0 * X(hgrant2=1))->X(locked=0));
assign sys_safe_err22 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock2 & controllable_hgrant2) | (~controllable_locked) );
// G( (decide=1 * hlock3=1 * X(hgrant3=1) )->X(locked=1));
assign sys_safe_err23 = ~( ~(~reg_controllable_ndecide & reg_i_hlock3 & controllable_hgrant3) | (controllable_locked) );
// G((decide=1 * hlock3=0 * X(hgrant3=1))->X(locked=0));
assign sys_safe_err24 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock3 & controllable_hgrant3) | (~controllable_locked) );
// G( (decide=0) -> ( ((hgrant0=0)<->X(hgrant0=0)) ));
assign sys_safe_err25 = ~( ~(reg_controllable_ndecide) | (reg_controllable_nhgrant0 ^~ controllable_nhgrant0) );
// G( (decide=0) -> ( ((hgrant1=0)<->X(hgrant1=0)) ));
assign sys_safe_err26 = ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant1 ^~ ~controllable_hgrant1) );
// G( (decide=0) -> ( ((hgrant2=0)<->X(hgrant2=0)) ));
assign sys_safe_err27 = ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant2 ^~ ~controllable_hgrant2) );
// G( (decide=0) -> ( ((hgrant3=0)<->X(hgrant3=0)) ));
assign sys_safe_err28 = ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant3 ^~ ~controllable_hgrant3) );
// G((decide=0)->(locked=0 <-> X(locked=0)));
assign sys_safe_err29 = ~( ~(reg_controllable_ndecide) | (~reg_controllable_locked ^~ ~controllable_locked) );
// G(((stateG10_1=1) * (((hgrant1=1)) * (hbusreq1=0)))->FALSE);
assign sys_safe_err30 = ~( ~(reg_stateG10_1 & (controllable_hgrant1 & ~i_hbusreq1)) | 0 );
// G(((stateG10_2=1) * (((hgrant2=1)) * (hbusreq2=0)))->FALSE);
assign sys_safe_err31 = ~( ~(reg_stateG10_2 & (controllable_hgrant2 & ~i_hbusreq2)) | 0 );
// G(((stateG10_3=1) * (((hgrant3=1)) * (hbusreq3=0)))->FALSE);
assign sys_safe_err32 = ~( ~(reg_stateG10_3 & (controllable_hgrant3 & ~i_hbusreq3)) | 0 );
// default master
// G((decide=1 * hbusreq0=0 * hbusreq1=0 * hbusreq2=0 * hbusreq3=0) -> X(hgrant0=1));
assign sys_safe_err33 = ~( ~(~reg_controllable_ndecide & (~reg_i_hbusreq0 & ~reg_i_hbusreq1 & ~reg_i_hbusreq2 & ~reg_i_hbusreq3)) | (~controllable_nhgrant0) );
// collecting together the safety error bits:
assign sys_safe_err = sys_safe_err0 |
sys_safe_err1 |
sys_safe_err2 |
sys_safe_err3 |
sys_safe_err4 |
sys_safe_err5 |
sys_safe_err6 |
sys_safe_err7 |
sys_safe_err8 |
sys_safe_err9 |
sys_safe_err10 |
sys_safe_err11 |
sys_safe_err12 |
sys_safe_err13 |
sys_safe_err14 |
sys_safe_err15 |
sys_safe_err16 |
sys_safe_err17 |
sys_safe_err18 |
sys_safe_err19 |
sys_safe_err20 |
sys_safe_err21 |
sys_safe_err22 |
sys_safe_err23 |
sys_safe_err24 |
sys_safe_err25 |
sys_safe_err26 |
sys_safe_err27 |
sys_safe_err28 |
sys_safe_err29 |
sys_safe_err30 |
sys_safe_err31 |
sys_safe_err32 |
sys_safe_err33;
// =============================================================
// ENV_FAIRNESS:
// =============================================================
// Assumption 1:
// G(F(stateA1=0));
assign env_fair0 = ~reg_stateA1;
// Assumption 2:
// G(F(hready=1));
assign env_fair1 = i_hready;
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: