-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathamba5f17n.aag
executable file
·1404 lines (1324 loc) · 32.7 KB
/
amba5f17n.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 658 26 49 1 583
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 882
58 10
60 48
62 14
64 46
66 18
68 967
70 1009
72 1010
74 1035
76 1036
78 6
80 42
82 1038
84 1059
86 26
88 24
90 8
92 34
94 22
96 1060
98 1071
100 1101
102 1123
104 36
106 20
108 52
110 1145
112 2
114 1146
116 38
118 1171
120 16
122 1247
124 1253
126 1259
128 1265
130 1271
132 1293
134 40
136 12
138 28
140 175
142 1315
144 44
146 1316
148 4
150 50
816
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 773 767
776 774 761
778 776 755
780 778 749
782 781 748
784 782 779
786 772 764
788 787 775
790 775 758
792 791 777
794 777 752
796 795 779
798 779 749
800 778 746
802 801 799
804 788 772
806 804 792
808 806 796
810 808 802
812 811 785
814 812 742
816 815 174
818 73 54
820 819 54
822 821 254
824 97 54
826 825 54
828 827 283
830 829 823
832 147 54
834 833 54
836 179 34
838 836 835
840 839 830
842 77 54
844 843 54
846 191 36
848 846 845
850 849 840
852 115 54
854 853 54
856 205 38
858 856 855
860 859 850
862 57 54
864 863 54
866 219 40
868 866 865
870 869 860
872 83 54
874 873 54
876 231 44
878 876 875
880 879 870
882 881 869
884 282 52
886 884 9
888 886 33
890 888 30
892 890 29
894 890 28
896 273 264
898 896 281
900 898 28
902 270 267
904 902 281
906 904 28
908 270 264
910 908 281
912 910 28
914 278 274
916 914 28
918 894 893
920 919 893
922 895 893
924 922 900
926 925 920
928 922 901
930 928 906
932 931 926
934 928 907
936 934 912
938 937 932
940 934 913
942 940 916
944 943 938
946 917 264
948 946 913
950 948 907
952 951 907
954 953 901
956 954 895
958 956 893
960 959 893
962 961 945
964 944 264
966 965 963
968 99 54
970 98 54
972 969 54
974 119 54
976 118 54
978 975 54
980 976 973
982 71 54
984 70 54
986 983 54
988 987 29
990 989 981
992 990 881
994 993 881
996 991 881
998 997 994
1000 991 989
1002 1000 881
1004 1002 999
1006 998 984
1008 1007 1005
1010 881 823
1012 917 270
1014 1012 913
1016 1014 907
1018 1017 907
1020 1019 901
1022 1021 901
1024 1023 895
1026 1025 895
1028 1027 893
1030 1028 945
1032 944 270
1034 1033 1031
1036 881 849
1038 881 879
1040 917 278
1042 1040 913
1044 1043 913
1046 1045 907
1048 1046 901
1050 1048 895
1052 1050 893
1054 1052 945
1056 944 278
1058 1057 1055
1060 881 829
1062 991 981
1064 1062 881
1066 1064 999
1068 998 970
1070 1069 1067
1072 52 9
1074 1072 33
1076 1074 31
1078 1076 257
1080 254 27
1082 1081 1079
1084 1077 254
1086 1085 1077
1088 254 26
1090 1087 257
1092 1088 254
1094 1093 1091
1096 1095 1083
1098 1082 254
1100 1099 1097
1102 667 5
1104 1102 37
1106 664 36
1108 1106 1105
1110 1109 1105
1112 1107 664
1114 1112 1105
1116 1115 1105
1118 1117 1111
1120 1110 664
1122 1121 1119
1124 679 11
1126 1124 39
1128 676 38
1130 1128 1127
1132 1131 1127
1134 1129 676
1136 1134 1127
1138 1137 1127
1140 1139 1133
1142 1132 676
1144 1143 1141
1146 881 859
1148 979 52
1150 1148 33
1152 1150 31
1154 976 27
1156 1154 1153
1158 1157 1153
1160 1155 976
1162 1160 1153
1164 1163 1153
1166 1165 1159
1168 1158 976
1170 1169 1167
1172 990 773
1174 991 770
1176 1175 1173
1178 1177 881
1180 770 767
1182 771 764
1184 1183 1181
1186 1185 990
1188 991 764
1190 1189 1187
1192 1191 881
1194 770 764
1196 1194 761
1198 1195 758
1200 1199 1197
1202 1201 990
1204 991 758
1206 1205 1203
1208 1207 881
1210 1194 758
1212 1210 755
1214 1211 752
1216 1215 1213
1218 1217 990
1220 991 752
1222 1221 1219
1224 1223 881
1226 1210 752
1228 1226 749
1230 1227 746
1232 1231 1229
1234 1233 990
1236 991 746
1238 1237 1235
1240 1239 881
1242 1178 995
1244 994 770
1246 1245 1243
1248 1192 995
1250 994 764
1252 1251 1249
1254 1208 995
1256 994 758
1258 1257 1255
1260 1224 995
1262 994 752
1264 1263 1261
1266 1240 995
1268 994 746
1270 1269 1267
1272 691 15
1274 1272 41
1276 688 40
1278 1276 1275
1280 1279 1275
1282 1277 688
1284 1282 1275
1286 1285 1275
1288 1287 1281
1290 1280 688
1292 1291 1289
1294 703 19
1296 1294 45
1298 700 44
1300 1298 1297
1302 1301 1297
1304 1299 700
1306 1304 1297
1308 1307 1297
1310 1309 1303
1312 1302 700
1314 1313 1311
1316 881 839
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_17
This file was written by ABC on Sat Aug 31 20:25:01 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 amba5f17.v ---gives--> amba5f17.mv
> abc -c "read_blif_mv amba5f17.mv; write_aiger -s amba5f17n.aig" ---gives--> amba5f17n.aig
> aigtoaig amba5f17n.aig amba5f17n.aag ---gives--> amba5f17n.aag (this file)
Content of amba5f17.v:
module amba_5_new_17(
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) )) );