-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathamba5f16unrealn.aag
executable file
·1389 lines (1309 loc) · 32.5 KB
/
amba5f16unrealn.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 643 26 49 1 568
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 852
58 10
60 48
62 14
64 46
66 18
68 937
70 979
72 980
74 1005
76 1006
78 6
80 42
82 1008
84 1029
86 26
88 24
90 8
92 34
94 22
96 1030
98 1041
100 1071
102 1093
104 36
106 20
108 52
110 1115
112 2
114 1116
116 38
118 1141
120 16
122 1217
124 1223
126 1229
128 1235
130 1241
132 1263
134 40
136 12
138 28
140 175
142 1285
144 44
146 1286
148 4
150 50
786
152 35 12
154 37 16
156 155 153
158 39 20
160 159 156
162 41 22
164 163 160
166 45 24
168 167 164
170 141 54
172 171 54
174 173 168
176 51 49
178 176 47
180 34 27
182 35 26
184 183 181
186 185 178
188 50 49
190 188 47
192 36 27
194 37 26
196 195 193
198 197 190
200 199 187
202 51 48
204 202 47
206 38 27
208 39 26
210 209 207
212 211 204
214 213 200
216 50 48
218 216 47
220 40 27
222 41 26
224 223 221
226 225 218
228 227 214
230 176 46
232 44 27
234 45 26
236 235 233
238 237 230
240 239 228
242 139 54
244 138 54
246 243 54
248 247 9
250 249 240
252 101 54
254 100 54
256 253 54
258 254 9
260 259 250
262 69 54
264 68 54
266 263 54
268 75 54
270 74 54
272 269 54
274 273 267
276 85 54
278 84 54
280 277 54
282 281 274
284 283 9
286 285 260
288 113 54
290 112 54
292 289 54
294 290 178
296 293 179
298 297 295
300 299 244
302 301 286
304 149 54
306 148 54
308 305 54
310 309 190
312 306 191
314 313 311
316 315 244
318 317 302
320 59 54
322 58 54
324 321 54
326 325 204
328 322 205
330 329 327
332 331 244
334 333 318
336 63 54
338 62 54
340 337 54
342 341 218
344 338 219
346 345 343
348 347 244
350 349 334
352 67 54
354 66 54
356 353 54
358 357 230
360 354 231
362 361 359
364 363 244
366 365 350
368 79 54
370 78 54
372 369 54
374 370 53
376 373 52
378 377 375
380 379 244
382 381 366
384 151 54
386 150 54
388 385 54
390 61 54
392 60 54
394 391 54
396 395 389
398 65 54
400 64 54
402 399 54
404 403 396
406 405 178
408 404 179
410 409 407
412 411 8
414 413 382
416 395 386
418 416 403
420 419 190
422 418 191
424 423 421
426 425 8
428 427 414
430 392 389
432 430 403
434 433 204
436 432 205
438 437 435
440 439 8
442 441 428
444 392 386
446 444 403
448 447 218
450 446 219
452 451 449
454 453 8
456 455 442
458 400 396
460 459 230
462 458 231
464 463 461
466 465 8
468 467 456
470 109 54
472 108 54
474 471 54
476 475 52
478 472 53
480 479 477
482 481 8
484 483 468
486 81 54
488 80 54
490 487 54
492 137 54
494 136 54
496 493 54
498 494 491
500 498 3
502 500 7
504 503 484
506 497 491
508 506 3
510 508 6
512 511 504
514 121 54
516 120 54
518 515 54
520 516 491
522 520 4
524 522 7
526 525 512
528 519 491
530 528 4
532 530 6
534 533 526
536 107 54
538 106 54
540 537 54
542 538 491
544 542 10
546 544 7
548 547 534
550 541 491
552 550 10
554 552 6
556 555 548
558 95 54
560 94 54
562 559 54
564 560 491
566 564 14
568 566 7
570 569 556
572 563 491
574 572 14
576 574 6
578 577 570
580 89 54
582 88 54
584 581 54
586 582 491
588 586 18
590 588 7
592 591 578
594 585 491
596 594 18
598 596 6
600 599 592
602 293 2
604 290 3
606 605 603
608 607 488
610 609 600
612 306 5
614 309 4
616 615 613
618 617 488
620 619 610
622 322 11
624 325 10
626 625 623
628 627 488
630 629 620
632 338 15
634 341 14
636 635 633
638 637 488
640 639 630
642 354 19
644 357 18
646 645 643
648 647 488
650 649 640
652 370 7
654 373 6
656 655 653
658 657 488
660 659 650
662 103 54
664 102 54
666 663 54
668 37 4
670 668 664
672 671 660
674 111 54
676 110 54
678 675 54
680 39 10
682 680 676
684 683 672
686 133 54
688 132 54
690 687 54
692 41 14
694 692 688
696 695 684
698 143 54
700 142 54
702 699 54
704 45 18
706 704 700
708 707 696
710 93 54
712 711 54
714 105 54
716 715 54
718 717 713
720 117 54
722 721 54
724 723 718
726 135 54
728 727 54
730 729 724
732 145 54
734 733 54
736 735 730
738 736 491
740 738 2
742 741 708
744 131 54
746 130 54
748 745 54
750 129 54
752 128 54
754 751 54
756 127 54
758 126 54
760 757 54
762 125 54
764 124 54
766 763 54
768 123 54
770 122 54
772 769 54
774 771 765
776 774 759
778 776 753
780 778 748
782 781 749
784 782 742
786 785 174
788 73 54
790 789 54
792 791 254
794 97 54
796 795 54
798 797 283
800 799 793
802 147 54
804 803 54
806 179 34
808 806 805
810 809 800
812 77 54
814 813 54
816 191 36
818 816 815
820 819 810
822 115 54
824 823 54
826 205 38
828 826 825
830 829 820
832 57 54
834 833 54
836 219 40
838 836 835
840 839 830
842 83 54
844 843 54
846 231 44
848 846 845
850 849 840
852 851 839
854 282 52
856 854 9
858 856 33
860 858 30
862 860 29
864 860 28
866 273 264
868 866 281
870 868 28
872 270 267
874 872 281
876 874 28
878 270 264
880 878 281
882 880 28
884 278 274
886 884 28
888 864 863
890 889 863
892 865 863
894 892 870
896 895 890
898 892 871
900 898 876
902 901 896
904 898 877
906 904 882
908 907 902
910 904 883
912 910 886
914 913 908
916 887 264
918 916 883
920 918 877
922 921 877
924 923 871
926 924 865
928 926 863
930 929 863
932 931 915
934 914 264
936 935 933
938 99 54
940 98 54
942 939 54
944 119 54
946 118 54
948 945 54
950 946 943
952 71 54
954 70 54
956 953 54
958 957 29
960 959 951
962 960 851
964 963 851
966 961 851
968 967 964
970 961 959
972 970 851
974 972 969
976 968 954
978 977 975
980 851 793
982 887 270
984 982 883
986 984 877
988 987 877
990 989 871
992 991 871
994 993 865
996 995 865
998 997 863
1000 998 915
1002 914 270
1004 1003 1001
1006 851 819
1008 851 849
1010 887 278
1012 1010 883
1014 1013 883
1016 1015 877
1018 1016 871
1020 1018 865
1022 1020 863
1024 1022 915
1026 914 278
1028 1027 1025
1030 851 799
1032 961 951
1034 1032 851
1036 1034 969
1038 968 940
1040 1039 1037
1042 52 9
1044 1042 33
1046 1044 31
1048 1046 257
1050 254 27
1052 1051 1049
1054 1047 254
1056 1055 1047
1058 254 26
1060 1057 257
1062 1058 254
1064 1063 1061
1066 1065 1053
1068 1052 254
1070 1069 1067
1072 667 5
1074 1072 37
1076 664 36
1078 1076 1075
1080 1079 1075
1082 1077 664
1084 1082 1075
1086 1085 1075
1088 1087 1081
1090 1080 664
1092 1091 1089
1094 679 11
1096 1094 39
1098 676 38
1100 1098 1097
1102 1101 1097
1104 1099 676
1106 1104 1097
1108 1107 1097
1110 1109 1103
1112 1102 676
1114 1113 1111
1116 851 829
1118 949 52
1120 1118 33
1122 1120 31
1124 946 27
1126 1124 1123
1128 1127 1123
1130 1125 946
1132 1130 1123
1134 1133 1123
1136 1135 1129
1138 1128 946
1140 1139 1137
1142 960 773
1144 961 770
1146 1145 1143
1148 1147 851
1150 770 767
1152 771 764
1154 1153 1151
1156 1155 960
1158 961 764
1160 1159 1157
1162 1161 851
1164 770 764
1166 1164 761
1168 1165 758
1170 1169 1167
1172 1171 960
1174 961 758
1176 1175 1173
1178 1177 851
1180 1164 758
1182 1180 755
1184 1181 752
1186 1185 1183
1188 1187 960
1190 961 752
1192 1191 1189
1194 1193 851
1196 1180 752
1198 1196 749
1200 1197 746
1202 1201 1199
1204 1203 960
1206 961 746
1208 1207 1205
1210 1209 851
1212 1148 965
1214 964 770
1216 1215 1213
1218 1162 965
1220 964 764
1222 1221 1219
1224 1178 965
1226 964 758
1228 1227 1225
1230 1194 965
1232 964 752
1234 1233 1231
1236 1210 965
1238 964 746
1240 1239 1237
1242 691 15
1244 1242 41
1246 688 40
1248 1246 1245
1250 1249 1245
1252 1247 688
1254 1252 1245
1256 1255 1245
1258 1257 1251
1260 1250 688
1262 1261 1259
1264 703 19
1266 1264 45
1268 700 44
1270 1268 1267
1272 1271 1267
1274 1269 700
1276 1274 1267
1278 1277 1267
1280 1279 1273
1282 1272 700
1284 1283 1281
1286 851 809
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 fair_cnt<3>_out
l38 fair_cnt<4>_out
l39 reg_stateG10_3_out
l40 reg_i_hbusreq3_out
l41 reg_i_hlock0_out
l42 reg_i_hready_out
l43 env_safe_err_happened_out
l44 reg_stateG10_4_out
l45 reg_i_hbusreq4_out
l46 sys_fair2done_out
l47 reg_controllable_hgrant1_out
l48 reg_controllable_hmaster0_out
o0 o_err
c
amba_5_new_16
This file was written by ABC on Sat Aug 31 20:25:03 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 amba5f16unreal.v ---gives--> amba5f16unreal.mv
> abc -c "read_blif_mv amba5f16unreal.mv; write_aiger -s amba5f16unrealn.aig" ---gives--> amba5f16unrealn.aig
> aigtoaig amba5f16unrealn.aig amba5f16unrealn.aag ---gives--> amba5f16unrealn.aag (this file)
Content of amba5f16unreal.v:
module amba_5_new_16(
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 [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_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 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)) ) );
assign sys_safe_err8 = ~( ~(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_err9 = ~( ~(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_err10 = ~( ~(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_err11 = ~( ~(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_err12 = ~( ~(reg_i_hready) | ( reg_controllable_hgrant4 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 ) ) );
// HMASTLOCK:
// G( (hready=1) -> (locked=0 <-> X(hmastlock=0) ) );
assign sys_safe_err13 = ~( ~(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_err14 = ~( ~(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_err15 = ~( ~(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_err16 = ~( ~(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_err17 = ~( ~(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_err18 = ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) & reg_controllable_hmaster2 ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 )) );