-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathamba5c4unrealn.aag
executable file
·1435 lines (1355 loc) · 32.5 KB
/
amba5c4unrealn.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 703 26 43 1 634
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 1
56 10
58 48
60 14
62 927
64 46
66 18
68 1011
70 1035
72 6
74 42
76 1055
78 26
80 24
82 8
84 34
86 22
88 1085
90 1107
92 36
94 20
96 52
98 1129
100 2
102 38
104 1153
106 16
108 1253
110 1259
112 1265
114 1345
116 1351
118 1357
120 1363
122 1385
124 40
126 12
128 28
130 163
132 1407
134 44
136 4
138 50
758
140 35 12
142 37 16
144 143 141
146 39 20
148 147 144
150 41 22
152 151 148
154 45 24
156 155 152
158 131 54
160 159 54
162 161 156
164 51 49
166 164 47
168 34 27
170 35 26
172 171 169
174 173 166
176 50 49
178 176 47
180 36 27
182 37 26
184 183 181
186 185 178
188 187 175
190 51 48
192 190 47
194 38 27
196 39 26
198 197 195
200 199 192
202 201 188
204 50 48
206 204 47
208 40 27
210 41 26
212 211 209
214 213 206
216 215 202
218 164 46
220 44 27
222 45 26
224 223 221
226 225 218
228 227 216
230 129 54
232 128 54
234 231 54
236 235 9
238 237 228
240 89 54
242 88 54
244 241 54
246 242 9
248 247 238
250 69 54
252 68 54
254 251 54
256 71 54
258 70 54
260 257 54
262 261 255
264 77 54
266 76 54
268 265 54
270 269 262
272 271 9
274 273 248
276 101 54
278 100 54
280 277 54
282 278 166
284 281 167
286 285 283
288 287 232
290 289 274
292 137 54
294 136 54
296 293 54
298 297 178
300 294 179
302 301 299
304 303 232
306 305 290
308 57 54
310 56 54
312 309 54
314 313 192
316 310 193
318 317 315
320 319 232
322 321 306
324 61 54
326 60 54
328 325 54
330 329 206
332 326 207
334 333 331
336 335 232
338 337 322
340 67 54
342 66 54
344 341 54
346 345 218
348 342 219
350 349 347
352 351 232
354 353 338
356 73 54
358 72 54
360 357 54
362 358 53
364 361 52
366 365 363
368 367 232
370 369 354
372 139 54
374 138 54
376 373 54
378 59 54
380 58 54
382 379 54
384 383 377
386 65 54
388 64 54
390 387 54
392 391 384
394 393 166
396 392 167
398 397 395
400 399 8
402 401 370
404 383 374
406 404 391
408 407 178
410 406 179
412 411 409
414 413 8
416 415 402
418 380 377
420 418 391
422 421 192
424 420 193
426 425 423
428 427 8
430 429 416
432 380 374
434 432 391
436 435 206
438 434 207
440 439 437
442 441 8
444 443 430
446 388 384
448 447 218
450 446 219
452 451 449
454 453 8
456 455 444
458 97 54
460 96 54
462 459 54
464 463 52
466 460 53
468 467 465
470 469 8
472 471 456
474 75 54
476 74 54
478 475 54
480 127 54
482 126 54
484 481 54
486 482 479
488 486 3
490 488 7
492 491 472
494 485 479
496 494 3
498 496 6
500 499 492
502 107 54
504 106 54
506 503 54
508 504 479
510 508 4
512 510 7
514 513 500
516 507 479
518 516 4
520 518 6
522 521 514
524 95 54
526 94 54
528 525 54
530 526 479
532 530 10
534 532 7
536 535 522
538 529 479
540 538 10
542 540 6
544 543 536
546 87 54
548 86 54
550 547 54
552 548 479
554 552 14
556 554 7
558 557 544
560 551 479
562 560 14
564 562 6
566 565 558
568 81 54
570 80 54
572 569 54
574 570 479
576 574 18
578 576 7
580 579 566
582 573 479
584 582 18
586 584 6
588 587 580
590 281 2
592 278 3
594 593 591
596 595 476
598 597 588
600 294 5
602 297 4
604 603 601
606 605 476
608 607 598
610 310 11
612 313 10
614 613 611
616 615 476
618 617 608
620 326 15
622 329 14
624 623 621
626 625 476
628 627 618
630 342 19
632 345 18
634 633 631
636 635 476
638 637 628
640 358 7
642 361 6
644 643 641
646 645 476
648 647 638
650 91 54
652 90 54
654 651 54
656 37 4
658 656 652
660 659 648
662 99 54
664 98 54
666 663 54
668 39 10
670 668 664
672 671 660
674 123 54
676 122 54
678 675 54
680 41 14
682 680 676
684 683 672
686 133 54
688 132 54
690 687 54
692 45 18
694 692 688
696 695 684
698 85 54
700 699 54
702 93 54
704 703 54
706 705 701
708 103 54
710 709 54
712 711 706
714 125 54
716 715 54
718 717 712
720 135 54
722 721 54
724 723 718
726 724 479
728 726 2
730 729 696
732 113 54
734 112 54
736 733 54
738 111 54
740 110 54
742 739 54
744 109 54
746 108 54
748 745 54
750 747 741
752 750 736
754 753 737
756 754 730
758 757 162
760 115 54
762 114 54
764 761 54
766 117 54
768 116 54
770 767 54
772 119 54
774 118 54
776 773 54
778 120 54
780 769 763
782 780 775
784 782 779
786 784 245
788 769 764
790 788 775
792 790 779
794 792 270
796 770 763
798 796 775
800 798 779
802 167 34
804 803 800
806 770 764
808 806 775
810 808 779
812 179 36
814 813 810
816 780 776
818 816 779
820 193 38
822 821 818
824 788 776
826 824 779
828 207 40
830 829 826
832 796 776
834 832 779
836 219 44
838 837 834
840 63 54
842 62 54
844 841 54
846 105 54
848 104 54
850 847 54
852 851 845
854 842 28
856 794 787
858 857 787
860 795 787
862 860 804
864 863 858
866 860 805
868 866 814
870 869 864
872 866 815
874 872 822
876 875 870
878 872 823
880 878 830
882 881 876
884 878 831
886 884 838
888 887 882
890 884 839
892 890 852
894 893 888
896 890 853
898 896 854
900 899 894
902 855 842
904 902 853
906 905 853
908 907 839
910 908 831
912 910 823
914 912 815
916 914 805
918 916 795
920 918 787
922 920 901
924 900 842
926 925 923
928 270 52
930 928 9
932 930 33
934 932 30
936 934 29
938 934 28
940 261 252
942 940 269
944 942 28
946 258 255
948 946 269
950 948 28
952 258 252
954 952 269
956 954 28
958 266 262
960 958 28
962 938 937
964 963 937
966 939 937
968 966 944
970 969 964
972 966 945
974 972 950
976 975 970
978 972 951
980 978 956
982 981 976
984 978 957
986 984 960
988 987 982
990 961 252
992 990 957
994 992 951
996 995 951
998 997 945
1000 998 939
1002 1000 937
1004 1003 937
1006 1005 989
1008 988 252
1010 1009 1007
1012 961 258
1014 1012 957
1016 1014 951
1018 1017 951
1020 1019 945
1022 1021 945
1024 1023 939
1026 1025 939
1028 1027 937
1030 1028 989
1032 988 258
1034 1033 1031
1036 961 266
1038 1036 957
1040 1039 957
1042 1041 951
1044 1042 945
1046 1044 939
1048 1046 937
1050 1048 989
1052 988 266
1054 1053 1051
1056 52 9
1058 1056 33
1060 1058 31
1062 1060 245
1064 242 27
1066 1065 1063
1068 1061 242
1070 1069 1061
1072 242 26
1074 1071 245
1076 1072 242
1078 1077 1075
1080 1079 1067
1082 1066 242
1084 1083 1081
1086 655 5
1088 1086 37
1090 652 36
1092 1090 1089
1094 1093 1089
1096 1091 652
1098 1096 1089
1100 1099 1089
1102 1101 1095
1104 1094 652
1106 1105 1103
1108 667 11
1110 1108 39
1112 664 38
1114 1112 1111
1116 1115 1111
1118 1113 664
1120 1118 1111
1122 1121 1111
1124 1123 1117
1126 1116 664
1128 1127 1125
1130 851 52
1132 1130 33
1134 1132 31
1136 848 27
1138 1136 1135
1140 1139 1135
1142 1137 848
1144 1142 1135
1146 1145 1135
1148 1147 1141
1150 1140 848
1152 1151 1149
1154 899 888
1156 854 749
1158 855 746
1160 1159 1157
1162 852 746
1164 1161 853
1166 1165 1163
1168 1167 839
1170 1168 831
1172 1170 823
1174 1172 815
1176 1174 805
1178 1176 795
1180 1178 787
1182 746 743
1184 747 740
1186 1185 1183
1188 1187 854
1190 855 740
1192 1191 1189
1194 852 740
1196 1193 853
1198 1197 1195
1200 1199 839
1202 1200 831
1204 1202 823
1206 1204 815
1208 1206 805
1210 1208 795
1212 1210 787
1214 746 740
1216 1214 737
1218 1215 734
1220 1219 1217
1222 1221 854
1224 855 734
1226 1225 1223
1228 852 734
1230 1227 853
1232 1231 1229
1234 1233 839
1236 1234 831
1238 1236 823
1240 1238 815
1242 1240 805
1244 1242 795
1246 1244 787
1248 1180 1155
1250 1154 746
1252 1251 1249
1254 1212 1155
1256 1154 740
1258 1257 1255
1260 1246 1155
1262 1154 734
1264 1263 1261
1266 839 762
1268 1266 831
1270 1268 823
1272 1271 823
1274 1273 815
1276 1274 805
1278 1277 805
1280 1279 795
1282 1280 787
1284 1283 787
1286 839 768
1288 1286 831
1290 1289 831
1292 1291 823
1294 1292 815
1296 1294 805
1298 1297 805
1300 1299 795
1302 1301 795
1304 1303 787
1306 839 774
1308 1306 831
1310 1309 831
1312 1311 823
1314 1313 823
1316 1315 815
1318 1317 815
1320 1319 805
1322 1320 795
1324 1322 787
1326 839 778
1328 1326 831
1330 1328 823
1332 1330 815
1334 1332 805
1336 1334 795
1338 1336 787
1340 1285 889
1342 888 762
1344 1343 1341
1346 1304 889
1348 888 768
1350 1349 1347
1352 1324 889
1354 888 774
1356 1355 1353
1358 1338 889
1360 888 778
1362 1361 1359
1364 679 15
1366 1364 41
1368 676 40
1370 1368 1367
1372 1371 1367
1374 1369 676
1376 1374 1367
1378 1377 1367
1380 1379 1373
1382 1372 676
1384 1383 1381
1386 691 19
1388 1386 45
1390 688 44
1392 1390 1389
1394 1393 1389
1396 1391 688
1398 1396 1389
1400 1399 1389
1402 1401 1395
1404 1394 688
1406 1405 1403
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 i_hlock3
i11 i_hlock4
i12 controllable_busreq
i13 i_hready
i14 i_hburst1
i15 i_hburst0
i16 i_hbusreq0
i17 i_hbusreq1
i18 i_hbusreq2
i19 i_hbusreq3
i20 controllable_ndecide
i21 i_hbusreq4
i22 controllable_hmaster2
i23 controllable_hmaster1
i24 controllable_hmaster0
i25 controllable_hmastlock
l0 n55
l1 reg_controllable_hgrant2_out
l2 reg_controllable_hmaster1_out
l3 reg_controllable_hgrant3_out
l4 next_env_fair_out
l5 reg_controllable_hmaster2_out
l6 reg_controllable_hgrant4_out
l7 reg_stateG3_0_out
l8 reg_stateG3_1_out
l9 reg_controllable_locked_out
l10 reg_controllable_ndecide_out
l11 reg_stateG3_2_out
l12 reg_controllable_busreq_out
l13 reg_i_hlock4_out
l14 reg_controllable_nstart_out
l15 reg_i_hbusreq0_out
l16 reg_i_hlock3_out
l17 reg_stateG2_out
l18 reg_stateG10_1_out
l19 reg_i_hbusreq1_out
l20 reg_i_hlock2_out
l21 reg_controllable_hmastlock_out
l22 reg_stateG10_2_out
l23 reg_controllable_nhgrant0_out
l24 reg_i_hbusreq2_out
l25 reg_stateA1_out
l26 reg_i_hlock1_out
l27 fair_cnt<0>_out
l28 fair_cnt<1>_out
l29 fair_cnt<2>_out
l30 next_sys_fair<0>_out
l31 next_sys_fair<1>_out
l32 next_sys_fair<2>_out
l33 next_sys_fair<3>_out
l34 reg_stateG10_3_out
l35 reg_i_hbusreq3_out
l36 reg_i_hlock0_out
l37 reg_i_hready_out
l38 env_safe_err_happened_out
l39 reg_stateG10_4_out
l40 reg_i_hbusreq4_out
l41 reg_controllable_hgrant1_out
l42 reg_controllable_hmaster0_out
o0 o_err
c
amba_5_new_4
This file was written by ABC on Sat Aug 31 20:24:50 2013
For information about AIGER format, refer to http://fmv.jku.at/aiger
-------------------------------
This AIGER file has been created by the following sequence of commands:
> vl2mv amba5c4unreal.v ---gives--> amba5c4unreal.mv
> abc -c "read_blif_mv amba5c4unreal.mv; write_aiger -s amba5c4unrealn.aig" ---gives--> amba5c4unrealn.aig
> aigtoaig amba5c4unrealn.aig amba5c4unrealn.aag ---gives--> amba5c4unrealn.aag (this file)
Content of amba5c4unreal.v:
module amba_5_new_4(
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_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_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_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_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_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_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 env_safe_err_happened;
reg next_env_fair;
reg [2:0] fair_cnt;
reg [3:0] next_sys_fair;
wire env_safe_err0;
wire env_safe_err1;
wire env_safe_err2;
wire env_safe_err3;
wire env_safe_err4;
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_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 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);
// 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;
// =============================================================
// 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)));
// Guarantee 1:
// G((hready=0) -> X(start=0));
assign sys_safe_err5 = ~( reg_i_hready | controllable_nstart );
// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err6 = ~( ~(reg_stateG2 & ~controllable_nstart) | 0 );