-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathamba5b4unrealn.aag
executable file
·1442 lines (1362 loc) · 33.7 KB
/
amba5b4unrealn.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 681 26 47 1 608
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 889
58 10
60 48
62 14
64 46
66 18
68 973
70 1019
72 1033
74 1057
76 1071
78 6
80 42
82 1085
84 1105
86 26
88 24
90 8
92 34
94 22
96 1119
98 1131
100 1161
102 1183
104 36
106 20
108 52
110 1205
112 2
114 1219
116 38
118 1243
120 16
122 1293
124 1299
126 1305
128 1327
130 40
132 12
134 28
136 171
138 1349
140 44
142 1363
144 4
146 50
766
148 35 12
150 37 16
152 151 149
154 39 20
156 155 152
158 41 22
160 159 156
162 45 24
164 163 160
166 137 54
168 167 54
170 169 164
172 51 49
174 172 47
176 34 27
178 35 26
180 179 177
182 181 174
184 50 49
186 184 47
188 36 27
190 37 26
192 191 189
194 193 186
196 195 183
198 51 48
200 198 47
202 38 27
204 39 26
206 205 203
208 207 200
210 209 196
212 50 48
214 212 47
216 40 27
218 41 26
220 219 217
222 221 214
224 223 210
226 172 46
228 44 27
230 45 26
232 231 229
234 233 226
236 235 224
238 135 54
240 134 54
242 239 54
244 243 9
246 245 236
248 101 54
250 100 54
252 249 54
254 250 9
256 255 246
258 69 54
260 68 54
262 259 54
264 75 54
266 74 54
268 265 54
270 269 263
272 85 54
274 84 54
276 273 54
278 277 270
280 279 9
282 281 256
284 113 54
286 112 54
288 285 54
290 286 174
292 289 175
294 293 291
296 295 240
298 297 282
300 145 54
302 144 54
304 301 54
306 305 186
308 302 187
310 309 307
312 311 240
314 313 298
316 59 54
318 58 54
320 317 54
322 321 200
324 318 201
326 325 323
328 327 240
330 329 314
332 63 54
334 62 54
336 333 54
338 337 214
340 334 215
342 341 339
344 343 240
346 345 330
348 67 54
350 66 54
352 349 54
354 353 226
356 350 227
358 357 355
360 359 240
362 361 346
364 79 54
366 78 54
368 365 54
370 366 53
372 369 52
374 373 371
376 375 240
378 377 362
380 147 54
382 146 54
384 381 54
386 61 54
388 60 54
390 387 54
392 391 385
394 65 54
396 64 54
398 395 54
400 399 392
402 401 174
404 400 175
406 405 403
408 407 8
410 409 378
412 391 382
414 412 399
416 415 186
418 414 187
420 419 417
422 421 8
424 423 410
426 388 385
428 426 399
430 429 200
432 428 201
434 433 431
436 435 8
438 437 424
440 388 382
442 440 399
444 443 214
446 442 215
448 447 445
450 449 8
452 451 438
454 396 392
456 455 226
458 454 227
460 459 457
462 461 8
464 463 452
466 109 54
468 108 54
470 467 54
472 471 52
474 468 53
476 475 473
478 477 8
480 479 464
482 81 54
484 80 54
486 483 54
488 133 54
490 132 54
492 489 54
494 490 487
496 494 3
498 496 7
500 499 480
502 493 487
504 502 3
506 504 6
508 507 500
510 121 54
512 120 54
514 511 54
516 512 487
518 516 4
520 518 7
522 521 508
524 515 487
526 524 4
528 526 6
530 529 522
532 107 54
534 106 54
536 533 54
538 534 487
540 538 10
542 540 7
544 543 530
546 537 487
548 546 10
550 548 6
552 551 544
554 95 54
556 94 54
558 555 54
560 556 487
562 560 14
564 562 7
566 565 552
568 559 487
570 568 14
572 570 6
574 573 566
576 89 54
578 88 54
580 577 54
582 578 487
584 582 18
586 584 7
588 587 574
590 581 487
592 590 18
594 592 6
596 595 588
598 289 2
600 286 3
602 601 599
604 603 484
606 605 596
608 302 5
610 305 4
612 611 609
614 613 484
616 615 606
618 318 11
620 321 10
622 621 619
624 623 484
626 625 616
628 334 15
630 337 14
632 631 629
634 633 484
636 635 626
638 350 19
640 353 18
642 641 639
644 643 484
646 645 636
648 366 7
650 369 6
652 651 649
654 653 484
656 655 646
658 103 54
660 102 54
662 659 54
664 37 4
666 664 660
668 667 656
670 111 54
672 110 54
674 671 54
676 39 10
678 676 672
680 679 668
682 129 54
684 128 54
686 683 54
688 41 14
690 688 684
692 691 680
694 139 54
696 138 54
698 695 54
700 45 18
702 700 696
704 703 692
706 93 54
708 707 54
710 105 54
712 711 54
714 713 709
716 117 54
718 717 54
720 719 714
722 131 54
724 723 54
726 725 720
728 141 54
730 729 54
732 731 726
734 732 487
736 734 2
738 737 704
740 127 54
742 126 54
744 741 54
746 125 54
748 124 54
750 747 54
752 123 54
754 122 54
756 753 54
758 755 749
760 758 744
762 761 745
764 762 738
766 765 170
768 73 54
770 72 54
772 769 54
774 773 250
776 97 54
778 96 54
780 777 54
782 781 279
784 783 775
786 143 54
788 142 54
790 787 54
792 175 34
794 792 791
796 795 784
798 77 54
800 76 54
802 799 54
804 187 36
806 804 803
808 807 796
810 115 54
812 114 54
814 811 54
816 201 38
818 816 815
820 819 808
822 57 54
824 56 54
826 823 54
828 215 40
830 828 827
832 831 820
834 83 54
836 82 54
838 835 54
840 227 44
842 840 839
844 843 832
846 773 253
848 781 278
850 849 847
852 793 791
854 853 850
856 805 803
858 857 854
860 817 815
862 861 858
864 829 827
866 865 862
868 841 839
870 869 866
872 871 845
874 873 845
876 871 831
878 870 824
880 879 877
882 881 845
884 882 875
886 874 824
888 887 885
890 278 52
892 890 9
894 892 33
896 894 30
898 896 29
900 896 28
902 269 260
904 902 277
906 904 28
908 266 263
910 908 277
912 910 28
914 266 260
916 914 277
918 916 28
920 274 270
922 920 28
924 900 899
926 925 899
928 901 899
930 928 906
932 931 926
934 928 907
936 934 912
938 937 932
940 934 913
942 940 918
944 943 938
946 940 919
948 946 922
950 949 944
952 923 260
954 952 919
956 954 913
958 957 913
960 959 907
962 960 901
964 962 899
966 965 899
968 967 951
970 950 260
972 971 969
974 99 54
976 98 54
978 975 54
980 119 54
982 118 54
984 981 54
986 982 979
988 71 54
990 70 54
992 989 54
994 993 29
996 995 987
998 870 845
1000 998 996
1002 1001 874
1004 998 997
1006 1005 1002
1008 997 995
1010 1008 870
1012 1010 845
1014 1012 1007
1016 1006 990
1018 1017 1015
1020 871 775
1022 870 770
1024 1023 1021
1026 1025 845
1028 1026 875
1030 874 770
1032 1031 1029
1034 923 266
1036 1034 919
1038 1036 913
1040 1039 913
1042 1041 907
1044 1043 907
1046 1045 901
1048 1047 901
1050 1049 899
1052 1050 951
1054 950 266
1056 1055 1053
1058 871 807
1060 870 800
1062 1061 1059
1064 1063 845
1066 1064 875
1068 874 800
1070 1069 1067
1072 871 843
1074 870 836
1076 1075 1073
1078 1077 845
1080 1078 875
1082 874 836
1084 1083 1081
1086 923 274
1088 1086 919
1090 1089 919
1092 1091 913
1094 1092 907
1096 1094 901
1098 1096 899
1100 1098 951
1102 950 274
1104 1103 1101
1106 871 783
1108 870 778
1110 1109 1107
1112 1111 845
1114 1112 875
1116 874 778
1118 1117 1115
1120 997 987
1122 1120 870
1124 1122 845
1126 1124 1007
1128 1006 976
1130 1129 1127
1132 52 9
1134 1132 33
1136 1134 31
1138 1136 253
1140 250 27
1142 1141 1139
1144 1137 250
1146 1145 1137
1148 250 26
1150 1147 253
1152 1148 250
1154 1153 1151
1156 1155 1143
1158 1142 250
1160 1159 1157
1162 663 5
1164 1162 37
1166 660 36
1168 1166 1165
1170 1169 1165
1172 1167 660
1174 1172 1165
1176 1175 1165
1178 1177 1171
1180 1170 660
1182 1181 1179
1184 675 11
1186 1184 39
1188 672 38
1190 1188 1187
1192 1191 1187
1194 1189 672
1196 1194 1187
1198 1197 1187
1200 1199 1193
1202 1192 672
1204 1203 1201
1206 871 819
1208 870 812
1210 1209 1207
1212 1211 845
1214 1212 875
1216 874 812
1218 1217 1215
1220 985 52
1222 1220 33
1224 1222 31
1226 982 27
1228 1226 1225
1230 1229 1225
1232 1227 982
1234 1232 1225
1236 1235 1225
1238 1237 1231
1240 1230 982
1242 1241 1239
1244 996 757
1246 997 754
1248 1247 1245
1250 1249 870
1252 1250 845
1254 754 751
1256 755 748
1258 1257 1255
1260 1259 996
1262 997 748
1264 1263 1261
1266 1265 870
1268 1266 845
1270 754 748
1272 1270 745
1274 1271 742
1276 1275 1273
1278 1277 996
1280 997 742
1282 1281 1279
1284 1283 870
1286 1284 845
1288 1252 1003
1290 1002 754
1292 1291 1289
1294 1268 1003
1296 1002 748
1298 1297 1295
1300 1286 1003
1302 1002 742
1304 1303 1301
1306 687 15
1308 1306 41
1310 684 40
1312 1310 1309
1314 1313 1309
1316 1311 684
1318 1316 1309
1320 1319 1309
1322 1321 1315
1324 1314 684
1326 1325 1323
1328 699 19
1330 1328 45
1332 696 44
1334 1332 1331
1336 1335 1331
1338 1333 696
1340 1338 1331
1342 1341 1331
1344 1343 1337
1346 1336 696
1348 1347 1345
1350 871 795
1352 870 788
1354 1353 1351
1356 1355 845
1358 1356 875
1360 874 788
1362 1361 1359
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 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_stateG3_1_out
l11 sys_fair3done_out
l12 reg_controllable_locked_out
l13 reg_controllable_ndecide_out
l14 sys_fair6done_out
l15 reg_stateG3_2_out
l16 reg_controllable_busreq_out
l17 reg_i_hlock4_out
l18 reg_controllable_nstart_out
l19 reg_i_hbusreq0_out
l20 reg_i_hlock3_out
l21 sys_fair1done_out
l22 env_fair0done_out
l23 reg_stateG2_out
l24 reg_stateG10_1_out
l25 reg_i_hbusreq1_out
l26 reg_i_hlock2_out
l27 reg_controllable_hmastlock_out
l28 reg_stateG10_2_out
l29 reg_controllable_nhgrant0_out
l30 sys_fair4done_out
l31 reg_i_hbusreq2_out
l32 reg_stateA1_out
l33 reg_i_hlock1_out
l34 fair_cnt<0>_out
l35 fair_cnt<1>_out
l36 fair_cnt<2>_out
l37 reg_stateG10_3_out
l38 reg_i_hbusreq3_out
l39 reg_i_hlock0_out
l40 reg_i_hready_out
l41 env_safe_err_happened_out
l42 reg_stateG10_4_out
l43 reg_i_hbusreq4_out
l44 sys_fair2done_out
l45 reg_controllable_hgrant1_out
l46 reg_controllable_hmaster0_out
o0 o_err
c
amba_5_new_4
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 amba5b4unreal.v ---gives--> amba5b4unreal.mv
> abc -c "read_blif_mv amba5b4unreal.mv; write_aiger -s amba5b4unrealn.aig" ---gives--> amba5b4unrealn.aig
> aigtoaig amba5b4unrealn.aig amba5b4unrealn.aag ---gives--> amba5b4unrealn.aag (this file)
Content of amba5b4unreal.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 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 [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_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 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);
// 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 );
// 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_err7 = (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)) ) );