-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathamba7b5y.aag
executable file
·1462 lines (1362 loc) · 38.2 KB
/
amba7b5y.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 527 32 57 1 438
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
56
58
60
62
64
66 1
68 870
70 10
72 874
74 56
76 60
78 14
80 876
82 58
84 18
86 899
88 950
90 952
92 32
94 22
96 971
98 972
100 6
102 50
104 30
106 974
108 26
110 981
112 34
114 28
116 8
118 42
120 24
122 982
124 984
126 993
128 996
130 44
132 20
134 64
136 1000
138 2
140 1002
142 46
144 1013
146 16
148 1020
150 1028
152 1038
154 1040
156 1044
158 48
160 12
162 36
164 209
166 1048
168 52
170 1050
172 4
174 1054
176 54
178 62
802
180 43 12
182 45 16
184 183 181
186 47 20
188 187 184
190 49 24
192 191 188
194 53 28
196 195 192
198 55 30
200 199 196
202 57 32
204 203 200
206 164 66
208 207 204
210 63 61
212 210 59
214 178 66
216 76 66
218 217 215
220 82 66
222 221 218
224 223 212
226 222 213
228 227 225
230 229 8
232 63 60
234 232 58
236 56 35
238 57 34
240 239 237
242 241 234
244 62 61
246 244 58
248 54 35
250 55 34
252 251 249
254 253 246
256 210 58
258 52 35
260 53 34
262 261 259
264 263 256
266 62 60
268 266 59
270 48 35
272 49 34
274 273 271
276 275 268
278 42 35
280 43 34
282 281 279
284 283 212
286 244 59
288 44 35
290 45 34
292 291 289
294 293 286
296 295 285
298 232 59
300 46 35
302 47 34
304 303 301
306 305 298
308 86 66
310 96 66
312 311 309
314 110 66
316 315 312
318 126 66
320 162 66
322 320 319
324 322 316
326 325 9
328 100 66
330 328 65
332 329 64
334 333 331
336 108 66
338 337 234
340 336 235
342 341 339
344 94 66
346 345 246
348 344 247
350 349 347
352 84 66
354 353 256
356 352 257
358 357 355
360 78 66
362 361 268
364 360 269
366 365 363
368 70 66
370 369 298
372 368 299
374 373 371
376 138 66
378 376 212
380 377 213
382 381 379
384 172 66
386 385 286
388 384 287
390 389 387
392 390 382
394 392 374
396 394 366
398 396 358
400 398 350
402 400 342
404 402 334
406 405 320
408 407 327
410 408 307
412 410 296
414 412 277
416 414 265
418 416 255
420 418 243
422 420 231
424 217 214
426 424 221
428 427 286
430 426 287
432 431 429
434 433 8
436 435 422
438 216 215
440 438 221
442 441 298
444 440 299
446 445 443
448 447 8
450 449 436
452 216 214
454 452 221
456 455 268
458 454 269
460 459 457
462 461 8
464 463 450
466 220 218
468 467 256
470 466 257
472 471 469
474 473 8
476 475 464
478 424 220
480 479 246
482 478 247
484 483 481
486 485 8
488 487 476
490 438 220
492 491 234
494 490 235
496 495 493
498 497 8
500 499 488
502 134 66
504 503 64
506 502 65
508 507 505
510 509 8
512 511 500
514 160 66
516 102 66
518 517 514
520 518 3
522 520 7
524 523 512
526 517 515
528 526 3
530 528 6
532 531 524
534 146 66
536 534 517
538 536 4
540 538 7
542 541 532
544 535 517
546 544 4
548 546 6
550 549 542
552 132 66
554 552 517
556 554 10
558 556 7
560 559 550
562 553 517
564 562 10
566 564 6
568 567 560
570 120 66
572 570 517
574 572 14
576 574 7
578 577 568
580 571 517
582 580 14
584 582 6
586 585 578
588 114 66
590 588 517
592 590 18
594 592 7
596 595 586
598 589 517
600 598 18
602 600 6
604 603 596
606 104 66
608 606 517
610 608 22
612 610 7
614 613 604
616 607 517
618 616 22
620 618 6
622 621 614
624 92 66
626 624 517
628 626 26
630 628 7
632 631 622
634 625 517
636 634 26
638 636 6
640 639 632
642 377 2
644 376 3
646 645 643
648 647 516
650 649 640
652 384 5
654 385 4
656 655 653
658 657 516
660 659 650
662 368 11
664 369 10
666 665 663
668 667 516
670 669 660
672 360 15
674 361 14
676 675 673
678 677 516
680 679 670
682 352 19
684 353 18
686 685 683
688 687 516
690 689 680
692 344 23
694 345 22
696 695 693
698 697 516
700 699 690
702 336 27
704 337 26
706 705 703
708 707 516
710 709 700
712 328 7
714 329 6
716 715 713
718 717 516
720 719 710
722 128 66
724 45 4
726 724 722
728 727 720
730 136 66
732 47 10
734 732 730
736 735 728
738 156 66
740 49 14
742 740 738
744 743 736
746 166 66
748 53 18
750 748 746
752 751 744
754 174 66
756 55 22
758 756 754
760 759 752
762 72 66
764 57 26
766 764 762
768 767 760
770 177 169
772 770 75
774 159 143
776 131 119
778 776 774
780 778 772
782 781 66
784 783 517
786 784 2
788 787 768
790 150 66
792 148 66
794 793 791
796 152 66
798 796 795
800 799 788
802 801 208
804 269 48
806 68 66
808 807 804
810 90 66
812 811 318
814 122 66
816 815 317
818 817 813
820 213 42
822 170 66
824 823 820
826 825 818
828 287 44
830 98 66
832 831 828
834 833 826
836 299 46
838 140 66
840 839 836
842 841 834
844 842 809
846 257 52
848 106 66
850 849 846
852 851 844
854 247 54
856 154 66
858 857 854
860 859 852
862 235 56
864 80 66
866 865 862
868 867 860
870 869 809
872 763 26
874 873 57
876 869 867
878 64 9
880 878 41
882 880 316
884 882 38
886 884 37
888 315 36
890 889 309
892 888 308
894 893 891
896 894 313
898 897 887
900 88 66
902 901 37
904 811 319
906 815 316
908 907 905
910 823 821
912 911 908
914 831 829
916 915 912
918 839 837
920 919 916
922 807 805
924 923 920
926 849 847
928 927 924
930 857 855
932 931 928
934 865 863
936 935 932
938 936 869
940 144 66
942 124 66
944 943 940
946 945 903
948 947 938
950 948 903
952 869 813
954 884 36
956 310 308
958 956 315
960 958 36
962 961 310
964 311 308
966 964 888
968 967 963
970 968 955
972 869 833
974 869 851
976 312 36
978 977 314
980 979 961
982 869 817
984 948 945
986 318 34
988 319 39
990 988 880
992 991 987
994 723 4
996 995 45
998 731 10
1000 999 47
1002 869 841
1004 941 64
1006 41 39
1008 1006 1004
1010 940 34
1012 1011 1009
1014 946 792
1016 947 793
1018 1017 1015
1020 1018 938
1022 1015 790
1024 1014 791
1026 1025 1023
1028 1027 938
1030 1014 790
1032 1031 797
1034 1030 796
1036 1035 1033
1038 1036 938
1040 869 859
1042 739 14
1044 1043 49
1046 747 18
1048 1047 53
1050 869 825
1052 755 22
1054 1053 55
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 controllable_hgrant5
i11 i_hlock3
i12 controllable_hgrant6
i13 i_hlock4
i14 i_hlock5
i15 i_hlock6
i16 controllable_busreq
i17 i_hready
i18 i_hburst1
i19 i_hburst0
i20 i_hbusreq0
i21 i_hbusreq1
i22 i_hbusreq2
i23 i_hbusreq3
i24 controllable_ndecide
i25 i_hbusreq4
i26 i_hbusreq5
i27 i_hbusreq6
i28 controllable_hmaster2
i29 controllable_hmaster1
i30 controllable_hmaster0
i31 controllable_hmastlock
l0 n67
l1 sys_fair5done_out
l2 reg_controllable_hgrant2_out
l3 reg_stateG10_6_out
l4 reg_i_hbusreq6_out
l5 reg_controllable_hmaster1_out
l6 reg_controllable_hgrant3_out
l7 sys_fair8done_out
l8 reg_controllable_hmaster2_out
l9 reg_controllable_hgrant4_out
l10 reg_stateG3_0_out
l11 env_fair1done_out
l12 sys_fair0done_out
l13 reg_i_hlock6_out
l14 reg_controllable_hgrant5_out
l15 reg_stateG3_1_out
l16 sys_fair3done_out
l17 reg_controllable_locked_out
l18 reg_controllable_ndecide_out
l19 reg_i_hlock5_out
l20 sys_fair6done_out
l21 reg_controllable_hgrant6_out
l22 reg_stateG3_2_out
l23 reg_controllable_busreq_out
l24 reg_i_hlock4_out
l25 reg_controllable_nstart_out
l26 reg_i_hbusreq0_out
l27 reg_i_hlock3_out
l28 sys_fair1done_out
l29 env_fair0done_out
l30 reg_stateG2_out
l31 reg_stateG10_1_out
l32 reg_i_hbusreq1_out
l33 reg_i_hlock2_out
l34 reg_controllable_hmastlock_out
l35 reg_stateG10_2_out
l36 reg_controllable_nhgrant0_out
l37 sys_fair4done_out
l38 reg_i_hbusreq2_out
l39 reg_stateA1_out
l40 reg_i_hlock1_out
l41 fair_cnt<0>_out
l42 fair_cnt<1>_out
l43 fair_cnt<2>_out
l44 sys_fair7done_out
l45 reg_stateG10_3_out
l46 reg_i_hbusreq3_out
l47 reg_i_hlock0_out
l48 reg_i_hready_out
l49 env_safe_err_happened_out
l50 reg_stateG10_4_out
l51 reg_i_hbusreq4_out
l52 sys_fair2done_out
l53 reg_controllable_hgrant1_out
l54 reg_stateG10_5_out
l55 reg_i_hbusreq5_out
l56 reg_controllable_hmaster0_out
o0 o_err
c
amba_7_new_5
This file was written by ABC on Sat Aug 31 20:24:40 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 amba7b5.v ---gives--> amba7b5.mv
> abc -c "read_blif_mv amba7b5.mv; strash; refactor; rewrite; dfraig; rewrite; dfraig; write_aiger -s amba7b5y.aig" ---gives--> amba7b5y.aig
> aigtoaig amba7b5y.aig amba7b5y.aag ---gives--> amba7b5y.aag (this file)
Content of amba7b5.v:
module amba_7_new_5(
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_hbusreq5,
i_hlock5,
i_hbusreq6,
i_hlock6,
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_hgrant5,
controllable_hgrant6,
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_hbusreq5;
input i_hlock5;
input i_hbusreq6;
input i_hlock6;
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_hgrant5;
input controllable_hgrant6;
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_i_hbusreq5;
reg reg_i_hlock5;
reg reg_i_hbusreq6;
reg reg_i_hlock6;
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_hgrant5;
reg reg_controllable_hgrant6;
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 reg_stateG10_5;
reg reg_stateG10_6;
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 sys_fair7done;
reg sys_fair8done;
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_err5;
wire env_safe_err6;
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_err41;
wire sys_safe_err42;
wire sys_safe_err43;
wire sys_safe_err44;
wire sys_safe_err45;
wire sys_safe_err46;
wire sys_safe_err47;
wire sys_safe_err48;
wire sys_safe_err49;
wire sys_safe_err50;
wire sys_safe_err51;
wire sys_safe_err52;
wire sys_safe_err53;
wire sys_safe_err54;
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 sys_fair7;
wire sys_fair8;
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);
// Assumption 3:
// G( hlock5=1 -> hbusreq5=1 );
assign env_safe_err5 = ~(~ i_hlock5 | i_hbusreq5);
// Assumption 3:
// G( hlock6=1 -> hbusreq6=1 );
assign env_safe_err6 = ~(~ i_hlock6 | i_hbusreq6);
// 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 |
env_safe_err5 |
env_safe_err6;
// =============================================================
// 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)));
// G((hmaster0=1) * (hmaster1=0) * (hmaster2=1) -> (hbusreq5=0 <-> busreq=0));
assign sys_safe_err5 = ~( ~( controllable_hmaster0 & ~(controllable_hmaster1) & controllable_hmaster2 )|(~i_hbusreq5 ^~ (~controllable_busreq)));
// G((hmaster0=0) * (hmaster1=1) * (hmaster2=1) -> (hbusreq6=0 <-> busreq=0));
assign sys_safe_err6 = ~( ~( ~(controllable_hmaster0) & controllable_hmaster1 & controllable_hmaster2 )|(~i_hbusreq6 ^~ (~controllable_busreq)));
// Guarantee 1:
// G((hready=0) -> X(start=0));
assign sys_safe_err7 = ~( reg_i_hready | controllable_nstart );
// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err8 = ~( ~(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_err9 = (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_err10 = ~( ~(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_err11 = ~( ~(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_err12 = ~( ~(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_err13 = ~( ~(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_err14 = ~( ~(reg_i_hready) | ( reg_controllable_hgrant4 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 ) ) );
// G( (hready=1) -> ( (hgrant5=1) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=1)) ) );
assign sys_safe_err15 = ~( ~(reg_i_hready) | ( reg_controllable_hgrant5 ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & controllable_hmaster2 ) ) );
// G( (hready=1) -> ( (hgrant6=1) <-> (X(hmaster0=0) * X(hmaster1=1) * X(hmaster2=1)) ) );
assign sys_safe_err16 = ~( ~(reg_i_hready) | ( reg_controllable_hgrant6 ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 & controllable_hmaster2 ) ) );
// HMASTLOCK:
// G( (hready=1) -> (locked=0 <-> X(hmastlock=0) ) );
assign sys_safe_err17 = ~( ~(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_err18 = ~( ~(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_err19 = ~( ~(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_err20 = ~( ~(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_err21 = ~( ~(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_err22 = ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) & reg_controllable_hmaster2 ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) & controllable_hmaster2 )) );
// Master 5:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=0) * (hmaster2=1)) <-> (X(hmaster0=1) * X(hmaster1=0) * X(hmaster2=1)) ) );
assign sys_safe_err23 = ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & ~(reg_controllable_hmaster1) & reg_controllable_hmaster2 ) ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) & controllable_hmaster2 )) );
// Master 6:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=1) * (hmaster2=1)) <-> (X(hmaster0=0) * X(hmaster1=1) * X(hmaster2=1)) ) );
assign sys_safe_err24 = ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & reg_controllable_hmaster1 & reg_controllable_hmaster2 ) ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 & controllable_hmaster2 )) );
// Guarantee 6.2:
// G( ((X(start=0))) -> ( (hmastlock=1) <-> X(hmastlock=1)) );
assign sys_safe_err25 = ~( ~(controllable_nstart) | ( reg_controllable_hmastlock ^~ controllable_hmastlock) );
// G( (decide=1 * hlock0=1 * X(hgrant0=1) )->X(locked=1));
assign sys_safe_err26 = ~( ~(~reg_controllable_ndecide & reg_i_hlock0 & ~controllable_nhgrant0) | (controllable_locked) );
// G((decide=1 * hlock0=0 * X(hgrant0=1))->X(locked=0));
assign sys_safe_err27 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock0 & ~controllable_nhgrant0) | (~controllable_locked) );
// G( (decide=1 * hlock1=1 * X(hgrant1=1) )->X(locked=1));
assign sys_safe_err28 = ~( ~(~reg_controllable_ndecide & reg_i_hlock1 & controllable_hgrant1) | (controllable_locked) );
// G((decide=1 * hlock1=0 * X(hgrant1=1))->X(locked=0));
assign sys_safe_err29 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock1 & controllable_hgrant1) | (~controllable_locked) );
// G( (decide=1 * hlock2=1 * X(hgrant2=1) )->X(locked=1));
assign sys_safe_err30 = ~( ~(~reg_controllable_ndecide & reg_i_hlock2 & controllable_hgrant2) | (controllable_locked) );
// G((decide=1 * hlock2=0 * X(hgrant2=1))->X(locked=0));
assign sys_safe_err31 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock2 & controllable_hgrant2) | (~controllable_locked) );
// G( (decide=1 * hlock3=1 * X(hgrant3=1) )->X(locked=1));
assign sys_safe_err32 = ~( ~(~reg_controllable_ndecide & reg_i_hlock3 & controllable_hgrant3) | (controllable_locked) );
// G((decide=1 * hlock3=0 * X(hgrant3=1))->X(locked=0));
assign sys_safe_err33 = ~( ~(~reg_controllable_ndecide & ~reg_i_hlock3 & controllable_hgrant3) | (~controllable_locked) );
// G( (decide=1 * hlock4=1 * X(hgrant4=1) )->X(locked=1));
assign sys_safe_err34 = ~( ~(~reg_controllable_ndecide & reg_i_hlock4 & controllable_hgrant4) | (controllable_locked) );