amba4f25y.aag

aag 347 22 43 1 282
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46 1
48 32
50 18
52 540
54 36
56 542
58 565
60 580
62 20
64 582
66 601
68 42
70 607
72 2
74 30
76 12
78 4
80 38
82 608
84 617
86 620
88 622
90 44
92 34
94 626
96 637
98 8
100 638
102 6
104 28
106 642
108 650
110 658
112 670
114 682
116 692
118 10
120 149
122 24
124 40
126 26
128 22
130 694
496
132 24 3
134 28 5
136 135 133
138 34 7
140 139 136
142 38 11
144 143 140
146 120 46
148 147 144
150 98 46
152 151 8
154 150 9
156 155 153
158 157 12
160 23 19
162 31 2
164 30 3
166 165 163
168 167 160
170 22 19
172 31 4
174 30 5
176 175 173
178 177 170
180 179 169
182 23 18
184 31 6
186 30 7
188 187 185
190 189 182
192 22 18
194 31 10
196 30 11
198 197 195
200 199 192
202 201 191
204 124 46
206 54 46
208 207 192
210 206 193
212 211 209
214 62 46
216 214 9
218 215 8
220 219 217
222 220 212
224 48 46
226 225 182
228 224 183
230 229 227
232 90 46
234 232 160
236 233 161
238 237 235
240 126 46
242 241 170
244 240 171
246 245 243
248 246 238
250 248 230
252 250 222
254 253 204
256 58 46
258 66 46
260 259 257
262 70 46
264 263 260
266 84 46
268 267 204
270 268 264
272 270 13
274 128 46
276 50 46
278 276 274
280 279 192
282 278 193
284 283 281
286 284 12
288 277 19
290 276 18
292 291 289
294 275 23
296 274 22
298 297 295
300 299 293
302 300 286
304 303 273
306 305 255
308 306 202
310 308 180
312 310 159
314 122 46
316 68 46
318 317 314
320 318 45
322 320 21
324 323 312
326 317 315
328 326 45
330 328 20
332 331 324
334 104 46
336 334 317
338 336 26
340 338 21
342 341 332
344 335 317
346 344 26
348 346 20
350 349 342
352 92 46
354 352 317
356 354 32
358 356 21
360 359 350
362 353 317
364 362 32
366 364 20
368 367 360
370 80 46
372 370 317
374 372 36
376 374 21
378 377 368
380 371 317
382 380 36
384 382 20
386 385 378
388 233 44
390 232 45
392 391 389
394 393 316
396 395 386
398 240 27
400 241 26
402 401 399
404 403 316
406 405 396
408 224 33
410 225 32
412 411 409
414 413 316
416 415 406
418 206 37
420 207 36
422 421 419
424 423 316
426 425 416
428 214 21
430 215 20
432 431 429
434 433 316
436 435 426
438 86 46
440 26 5
442 440 438
444 443 436
446 94 46
448 32 7
450 448 446
452 451 444
454 106 46
456 36 11
458 456 454
460 459 452
462 79 73
464 119 103
466 464 462
468 467 46
470 469 317
472 470 44
474 473 460
476 114 46
478 110 46
480 108 46
482 481 479
484 112 46
486 485 482
488 116 46
490 488 487
492 490 476
494 493 474
496 495 148
498 193 10
500 52 46
502 501 498
504 56 46
506 505 266
508 82 46
510 509 265
512 511 507
514 161 2
516 130 46
518 517 514
520 519 512
522 171 4
524 64 46
526 525 522
528 527 520
530 183 6
532 100 46
534 533 530
536 535 528
538 536 503
540 539 503
542 539 507
544 13 8
546 544 17
548 546 264
550 548 14
552 550 41
554 263 40
556 555 257
558 554 256
560 559 557
562 560 261
564 563 553
566 60 46
568 567 41
570 96 46
572 88 46
574 573 570
576 575 569
578 577 539
580 578 569
582 539 527
584 550 40
586 258 256
588 586 263
590 588 40
592 591 258
594 259 256
596 594 554
598 597 593
600 598 585
602 260 40
604 603 262
606 605 591
608 539 511
610 266 30
612 267 15
614 612 546
616 615 611
618 439 26
620 619 5
622 578 575
624 447 32
626 625 7
628 571 8
630 17 15
632 630 628
634 570 30
636 635 633
638 539 535
640 455 36
642 641 11
644 576 480
646 577 481
648 647 645
650 648 539
652 645 478
654 644 479
656 655 653
658 657 539
660 480 478
662 660 576
664 663 484
666 662 485
668 667 665
670 669 539
672 660 484
674 672 576
676 675 476
678 674 477
680 679 677
682 681 539
684 674 476
686 685 489
688 684 488
690 689 687
692 690 539
694 539 519
i0 i_hbusreq0
i1 i_hbusreq1
i2 i_hbusreq2
i3 controllable_hmastlock
i4 i_hbusreq3
i5 controllable_nstart
i6 i_hburst1
i7 i_hburst0
i8 controllable_hmaster1
i9 controllable_locked
i10 controllable_hmaster0
i11 i_hlock0
i12 controllable_hgrant1
i13 i_hlock1
i14 controllable_busreq
i15 controllable_hgrant2
i16 i_hlock2
i17 controllable_hgrant3
i18 i_hlock3
i19 i_hready
i20 controllable_ndecide
i21 controllable_nhgrant0
l0 n47
l1 reg_controllable_hgrant2_out
l2 reg_controllable_hmaster1_out
l3 sys_fair5done_out
l4 reg_controllable_hgrant3_out
l5 sys_fair0done_out
l6 reg_stateG3_0_out
l7 env_fair1done_out
l8 reg_controllable_locked_out
l9 sys_fair3done_out
l10 reg_stateG3_1_out
l11 reg_controllable_ndecide_out
l12 reg_stateG3_2_out
l13 reg_i_hbusreq0_out
l14 reg_controllable_busreq_out
l15 reg_controllable_nstart_out
l16 reg_i_hbusreq1_out
l17 reg_i_hlock3_out
l18 sys_fair1done_out
l19 reg_stateG2_out
l20 reg_stateG10_1_out
l21 env_fair0done_out
l22 reg_controllable_nhgrant0_out
l23 reg_i_hlock2_out
l24 reg_stateG10_2_out
l25 reg_stateA1_out
l26 reg_controllable_hmastlock_out
l27 sys_fair4done_out
l28 reg_i_hbusreq2_out
l29 reg_i_hlock1_out
l30 reg_stateG10_3_out
l31 fair_cnt<0>_out
l32 fair_cnt<1>_out
l33 fair_cnt<2>_out
l34 fair_cnt<3>_out
l35 fair_cnt<4>_out
l36 reg_i_hbusreq3_out
l37 env_safe_err_happened_out
l38 reg_i_hlock0_out
l39 reg_i_hready_out
l40 reg_controllable_hgrant1_out
l41 reg_controllable_hmaster0_out
l42 sys_fair2done_out
o0 o_err
c
amba_4_new_25
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 amba4f25.v   ---gives--> amba4f25.mv
> abc -c "read_blif_mv amba4f25.mv; strash; refactor; rewrite; dfraig; rewrite; dfraig; write_aiger -s amba4f25y.aig"   ---gives--> amba4f25y.aig
> aigtoaig amba4f25y.aig amba4f25y.aag   ---gives--> amba4f25y.aag (this file)
Content of amba4f25.v:
module amba_4_new_25(
        o_err,
        i_clk,
        i_hready,
        i_hbusreq0,
        i_hlock0,
        i_hbusreq1,
        i_hlock1,
        i_hbusreq2,
        i_hlock2,
        i_hbusreq3,
        i_hlock3,
        i_hburst0,
        i_hburst1,
        controllable_hmaster0,
        controllable_hmaster1,
        controllable_hmastlock,
        controllable_nstart,
        controllable_ndecide,
        controllable_locked,
        controllable_nhgrant0,
        controllable_hgrant1,
        controllable_hgrant2,
        controllable_hgrant3,
        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_hburst0;
input i_hburst1;
input controllable_hmaster0;
input controllable_hmaster1;
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_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_controllable_hmaster0;
reg reg_controllable_hmaster1;
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_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 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 [4:0] fair_cnt;

wire env_safe_err0;
wire env_safe_err1;
wire env_safe_err2;
wire env_safe_err3;
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_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 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);

// collecting together the safety error bits:
assign env_safe_err = env_safe_err0 |
                      env_safe_err1 |
                      env_safe_err2 |
                      env_safe_err3;

// =============================================================
//                        SYS_TRANSITION:
// =============================================================
// G((hmaster0=0) * (hmaster1=0) -> (hbusreq0=0 <-> busreq=0));
assign sys_safe_err0 =  ~( ~( ~(controllable_hmaster0) & ~(controllable_hmaster1) )|(~i_hbusreq0 ^~ (~controllable_busreq)));

// G((hmaster0=1) * (hmaster1=0) -> (hbusreq1=0 <-> busreq=0));
assign sys_safe_err1 =  ~( ~( controllable_hmaster0 & ~(controllable_hmaster1) )|(~i_hbusreq1 ^~ (~controllable_busreq)));

// G((hmaster0=0) * (hmaster1=1) -> (hbusreq2=0 <-> busreq=0));
assign sys_safe_err2 =  ~( ~( ~(controllable_hmaster0) & controllable_hmaster1 )|(~i_hbusreq2 ^~ (~controllable_busreq)));

// G((hmaster0=1) * (hmaster1=1) -> (hbusreq3=0 <-> busreq=0));
assign sys_safe_err3 =  ~( ~( controllable_hmaster0 & controllable_hmaster1 )|(~i_hbusreq3 ^~ (~controllable_busreq)));

// Guarantee 1:
// G((hready=0) -> X(start=0));
assign sys_safe_err4 =  ~( reg_i_hready | controllable_nstart );

// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err5 =  ~( ~(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_err6 =  (reg_stateG3_0 | reg_stateG3_1 | reg_stateG3_2) & ~controllable_nstart;

// G( (hready=1) -> (   (hgrant0=1) <-> (X(hmaster0=0) * X(hmaster1=0))  ) );
assign sys_safe_err7 =  ~( ~(reg_i_hready) | ( ~reg_controllable_nhgrant0 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) ) ) );

// G( (hready=1) -> (   (hgrant1=1) <-> (X(hmaster0=1) * X(hmaster1=0))  ) );
assign sys_safe_err8 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant1 ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) ) ) );

// G( (hready=1) -> (   (hgrant2=1) <-> (X(hmaster0=0) * X(hmaster1=1))  ) );
assign sys_safe_err9 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant2 ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 ) ) );

// G( (hready=1) -> (   (hgrant3=1) <-> (X(hmaster0=1) * X(hmaster1=1))  ) );
assign sys_safe_err10 =  ~( ~(reg_i_hready) | ( reg_controllable_hgrant3 ^~ ( controllable_hmaster0 & controllable_hmaster1 ) ) );

// HMASTLOCK:
// G(  (hready=1) -> (locked=0 <-> X(hmastlock=0) ) );
assign sys_safe_err11 =  ~( ~(reg_i_hready) | (~reg_controllable_locked ^~ ~controllable_hmastlock) );

// Master 0:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=0)) <-> (X(hmaster0=0) * X(hmaster1=0)) ) );
assign sys_safe_err12 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & ~(reg_controllable_hmaster1) ) ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) )) );

// Master 1:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=0)) <-> (X(hmaster0=1) * X(hmaster1=0)) ) );
assign sys_safe_err13 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & ~(reg_controllable_hmaster1) ) ^~ ( controllable_hmaster0 & ~(controllable_hmaster1) )) );

// Master 2:
// G( X(start=0) -> ( ((hmaster0=0) * (hmaster1=1)) <-> (X(hmaster0=0) * X(hmaster1=1)) ) );
assign sys_safe_err14 =  ~( ~(controllable_nstart) | ( ( ~(reg_controllable_hmaster0) & reg_controllable_hmaster1 ) ^~ ( ~(controllable_hmaster0) & controllable_hmaster1 )) );

// Master 3:
// G( X(start=0) -> ( ((hmaster0=1) * (hmaster1=1)) <-> (X(hmaster0=1) * X(hmaster1=1)) ) );
assign sys_safe_err15 =  ~( ~(controllable_nstart) | ( ( reg_controllable_hmaster0 & reg_controllable_hmaster1 ) ^~ ( controllable_hmaster0 & controllable_hmaster1 )) );

// Guarantee 6.2:
// G( ((X(start=0))) -> ( (hmastlock=1) <-> X(hmastlock=1)) );
assign sys_safe_err16 =  ~( ~(controllable_nstart) | ( reg_controllable_hmastlock ^~ controllable_hmastlock) );

// G( (decide=1  *  hlock0=1  *  X(hgrant0=1) )->X(locked=1));
assign sys_safe_err17 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock0 & ~controllable_nhgrant0) | (controllable_locked) );

// G((decide=1  *  hlock0=0  *  X(hgrant0=1))->X(locked=0));
assign sys_safe_err18 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock0 & ~controllable_nhgrant0) | (~controllable_locked) );

// G( (decide=1  *  hlock1=1  *  X(hgrant1=1) )->X(locked=1));
assign sys_safe_err19 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock1 & controllable_hgrant1) | (controllable_locked) );

// G((decide=1  *  hlock1=0  *  X(hgrant1=1))->X(locked=0));
assign sys_safe_err20 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock1 & controllable_hgrant1) | (~controllable_locked) );

// G( (decide=1  *  hlock2=1  *  X(hgrant2=1) )->X(locked=1));
assign sys_safe_err21 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock2 & controllable_hgrant2) | (controllable_locked) );

// G((decide=1  *  hlock2=0  *  X(hgrant2=1))->X(locked=0));
assign sys_safe_err22 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock2 & controllable_hgrant2) | (~controllable_locked) );

// G( (decide=1  *  hlock3=1  *  X(hgrant3=1) )->X(locked=1));
assign sys_safe_err23 =  ~( ~(~reg_controllable_ndecide & reg_i_hlock3 & controllable_hgrant3) | (controllable_locked) );

// G((decide=1  *  hlock3=0  *  X(hgrant3=1))->X(locked=0));
assign sys_safe_err24 =  ~( ~(~reg_controllable_ndecide & ~reg_i_hlock3 & controllable_hgrant3) | (~controllable_locked) );

// G( (decide=0) -> (  ((hgrant0=0)<->X(hgrant0=0))  ));
assign sys_safe_err25 =  ~( ~(reg_controllable_ndecide) | (reg_controllable_nhgrant0 ^~ controllable_nhgrant0) );

// G( (decide=0) -> (  ((hgrant1=0)<->X(hgrant1=0))  ));
assign sys_safe_err26 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant1 ^~ ~controllable_hgrant1) );

// G( (decide=0) -> (  ((hgrant2=0)<->X(hgrant2=0))  ));
assign sys_safe_err27 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant2 ^~ ~controllable_hgrant2) );

// G( (decide=0) -> (  ((hgrant3=0)<->X(hgrant3=0))  ));
assign sys_safe_err28 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_hgrant3 ^~ ~controllable_hgrant3) );

// G((decide=0)->(locked=0 <-> X(locked=0)));
assign sys_safe_err29 =  ~( ~(reg_controllable_ndecide) | (~reg_controllable_locked ^~ ~controllable_locked) );

// G(((stateG10_1=1) * (((hgrant1=1)) * (hbusreq1=0)))->FALSE);
assign sys_safe_err30 =  ~( ~(reg_stateG10_1 & (controllable_hgrant1 & ~i_hbusreq1)) | 0 );

// G(((stateG10_2=1) * (((hgrant2=1)) * (hbusreq2=0)))->FALSE);
assign sys_safe_err31 =  ~( ~(reg_stateG10_2 & (controllable_hgrant2 & ~i_hbusreq2)) | 0 );

// G(((stateG10_3=1) * (((hgrant3=1)) * (hbusreq3=0)))->FALSE);
assign sys_safe_err32 =  ~( ~(reg_stateG10_3 & (controllable_hgrant3 & ~i_hbusreq3)) | 0 );

// default master
// G((decide=1  *  hbusreq0=0  *  hbusreq1=0  *  hbusreq2=0  *  hbusreq3=0) -> X(hgrant0=1));
assign sys_safe_err33 =  ~( ~(~reg_controllable_ndecide & (~reg_i_hbusreq0 & ~reg_i_hbusreq1 & ~reg_i_hbusreq2 & ~reg_i_hbusreq3)) | (~controllable_nhgrant0) );

// collecting together the safety error bits:
assign sys_safe_err = sys_safe_err0 |
                      sys_safe_err1 |
                      sys_safe_err2 |
                      sys_safe_err3 |
                      sys_safe_err4 |
                      sys_safe_err5 |
                      sys_safe_err6 |
                      sys_safe_err7 |
                      sys_safe_err8 |
                      sys_safe_err9 |
                      sys_safe_err10 |
                      sys_safe_err11 |
                      sys_safe_err12 |
                      sys_safe_err13 |
                      sys_safe_err14 |
                      sys_safe_err15 |
                      sys_safe_err16 |
                      sys_safe_err17 |
                      sys_safe_err18 |
                      sys_safe_err19 |
                      sys_safe_err20 |
                      sys_safe_err21 |
                      sys_safe_err22 |
                      sys_safe_err23 |
                      sys_safe_err24 |
                      sys_safe_err25 |
                      sys_safe_err26 |
                      sys_safe_err27 |
                      sys_safe_err28 |
                      sys_safe_err29 |
                      sys_safe_err30 |
                      sys_safe_err31 |
                      sys_safe_err32 |
                      sys_safe_err33;

// =============================================================
//                          ENV_FAIRNESS:
// =============================================================
// Assumption 1: 
// G(F(stateA1=0));
assign env_fair0 =  ~reg_stateA1;

// Assumption 2:
// G(F(hready=1));
assign env_fair1 =  i_hready;

assign all_env_fair_fulfilled = (env_fair0done | env_fair0) &
                                (env_fair1done | env_fair1);

// =============================================================
//                          SYS_FAIRNESS:
// =============================================================
// Guarantee 2:
// G(F(stateG2=0));
assign sys_fair0 = ~reg_stateG2;

// Guarantee 3:
// G(F((stateG3_0=0)  *  (stateG3_1=0)  *  (stateG3_2=0)));
assign sys_fair1 =  (~reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2);

// G(F(((hmaster0=0) * (hmaster1=0))  |  hbusreq0=0));
assign sys_fair2 =  ( ~(controllable_hmaster0) & ~(controllable_hmaster1) ) | ~i_hbusreq0;

// G(F(((hmaster0=1) * (hmaster1=0))  |  hbusreq1=0));
assign sys_fair3 =  ( controllable_hmaster0 & ~(controllable_hmaster1) ) | ~i_hbusreq1;

// G(F(((hmaster0=0) * (hmaster1=1))  |  hbusreq2=0));
assign sys_fair4 =  ( ~(controllable_hmaster0) & controllable_hmaster1 ) | ~i_hbusreq2;

// G(F(((hmaster0=1) * (hmaster1=1))  |  hbusreq3=0));
assign sys_fair5 =  ( controllable_hmaster0 & controllable_hmaster1 ) | ~i_hbusreq3;

assign all_sys_fair_fulfilled = (sys_fair0done | sys_fair0) &
                                (sys_fair1done | sys_fair1) &
                                (sys_fair2done | sys_fair2) &
                                (sys_fair3done | sys_fair3) &
                                (sys_fair4done | sys_fair4) &
                                (sys_fair5done | sys_fair5);
assign fair_err = (fair_cnt >= 5'b11001);

// computing the error output bit:
assign o_err = ~env_safe_err & ~env_safe_err_happened & (sys_safe_err | fair_err);

initial
 begin
  reg_i_hready = 0;
  reg_i_hbusreq0 = 0;
  reg_i_hlock0 = 0;
  reg_i_hbusreq1 = 0;
  reg_i_hlock1 = 0;
  reg_i_hbusreq2 = 0;
  reg_i_hlock2 = 0;
  reg_i_hbusreq3 = 0;
  reg_i_hlock3 = 0;
  reg_controllable_hmaster0 = 0;
  reg_controllable_hmaster1 = 0;
  reg_controllable_hmastlock = 0;
  reg_controllable_nstart = 0;
  reg_controllable_ndecide = 0;
  reg_controllable_locked = 0;
  reg_controllable_nhgrant0 = 0;
  reg_controllable_hgrant1 = 0;
  reg_controllable_hgrant2 = 0;
  reg_controllable_hgrant3 = 0;
  reg_controllable_busreq = 0;
  reg_stateA1 = 0;
  reg_stateG2 = 0;
  reg_stateG3_0 = 0;
  reg_stateG3_1 = 0;
  reg_stateG3_2 = 0;
  reg_stateG10_1 = 0;
  reg_stateG10_2 = 0;
  reg_stateG10_3 = 0;
  env_safe_err_happened = 0;
  env_fair0done = 0;
  env_fair1done = 0;
  sys_fair0done = 0;
  sys_fair1done = 0;
  sys_fair2done = 0;
  sys_fair3done = 0;
  sys_fair4done = 0;
  sys_fair5done = 0;
  fair_cnt = 0;
 end


always @(posedge i_clk)
 begin
   // We remember if an environment error occurred:
   env_safe_err_happened = env_safe_err_happened | env_safe_err;

   // Updating the fairness counters: 
   if(all_sys_fair_fulfilled)
    begin
      env_fair0done = 0;
      env_fair1done = 0;
      sys_fair0done = 0;
      sys_fair1done = 0;
      sys_fair2done = 0;
      sys_fair3done = 0;
      sys_fair4done = 0;
      sys_fair5done = 0;
      fair_cnt = 0;
    end
   else
    begin
      sys_fair0done = sys_fair0done | sys_fair0;
      sys_fair1done = sys_fair1done | sys_fair1;
      sys_fair2done = sys_fair2done | sys_fair2;
      sys_fair3done = sys_fair3done | sys_fair3;
      sys_fair4done = sys_fair4done | sys_fair4;
      sys_fair5done = sys_fair5done | sys_fair5;
      if(all_env_fair_fulfilled)
       begin
         env_fair0done = 0;
         env_fair1done = 0;
         fair_cnt = fair_cnt + 1;
       end
      else
       begin
         env_fair0done = env_fair0done | env_fair0;
         env_fair1done = env_fair1done | env_fair1;
       end
    end

   // Updating the automata: 
   // Automaton A1: 
   if(~reg_stateA1 & controllable_hmastlock & ~i_hburst0 & ~i_hburst1)
    begin
      reg_stateA1 = 1'b1;
    end
   else if(reg_stateA1 & ~controllable_busreq)
    begin
      reg_stateA1 = 1'b0;
    end

   // Automaton G2: 
   if(~reg_stateG2)
    begin
      if(controllable_hmastlock & ~controllable_nstart & ~i_hburst0 & ~i_hburst1)
       begin
         reg_stateG2 = 1'b1;
       end
    end
   else // if(reg_stateG2)
    begin
      if(~controllable_busreq)
       begin
         reg_stateG2 = 1'b0;
       end
    end

   // Automaton G3: 
   if(~reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2 & controllable_hmastlock & ~controllable_nstart &  ~i_hburst0 & i_hburst1 & ~i_hready)
    begin
      reg_stateG3_0 = 1'b1;
      reg_stateG3_1 = 1'b0;
      reg_stateG3_2 = 1'b0;
    end
   else if(~reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2 & controllable_hmastlock & ~controllable_nstart &  ~i_hburst0 & i_hburst1 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b1;
      reg_stateG3_2 = 1'b0;
    end
   else if(reg_stateG3_0 & ~reg_stateG3_1 & ~reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b1;
      reg_stateG3_2 = 1'b0;
    end
   else if(~reg_stateG3_0 & reg_stateG3_1 & ~reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b1;
      reg_stateG3_1 = 1'b1;
      reg_stateG3_2 = 1'b0;
    end
   else if(reg_stateG3_0 & reg_stateG3_1 & ~reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b0;
      reg_stateG3_2 = 1'b1;
    end
   else if(~reg_stateG3_0 & ~reg_stateG3_1 & reg_stateG3_2 & i_hready)
    begin
      reg_stateG3_0 = 1'b0;
      reg_stateG3_1 = 1'b0;
      reg_stateG3_2 = 1'b0;
    end

   // Automaton G10_1: 
   if(~reg_stateG10_1 & ~controllable_hgrant1 & ~i_hbusreq1)
    begin
      reg_stateG10_1 = 1'b1;
    end
   else if(reg_stateG10_1 & i_hbusreq1)
    begin
      reg_stateG10_1 = 1'b0;
    end

   // Automaton G10_2: 
   if(~reg_stateG10_2 & ~controllable_hgrant2 & ~i_hbusreq2)
    begin
      reg_stateG10_2 = 1'b1;
    end
   else if(reg_stateG10_2 & i_hbusreq2)
    begin
      reg_stateG10_2 = 1'b0;
    end

   // Automaton G10_3: 
   if(~reg_stateG10_3 & ~controllable_hgrant3 & ~i_hbusreq3)
    begin
      reg_stateG10_3 = 1'b1;
    end
   else if(reg_stateG10_3 & i_hbusreq3)
    begin
      reg_stateG10_3 = 1'b0;
    end

   // Latching the previous input:
   reg_i_hready =  i_hready;
   reg_i_hbusreq0 =  i_hbusreq0;
   reg_i_hlock0 =  i_hlock0;
   reg_i_hbusreq1 =  i_hbusreq1;
   reg_i_hlock1 =  i_hlock1;
   reg_i_hbusreq2 =  i_hbusreq2;
   reg_i_hlock2 =  i_hlock2;
   reg_i_hbusreq3 =  i_hbusreq3;
   reg_i_hlock3 =  i_hlock3;
   reg_controllable_hmaster0 =  controllable_hmaster0;
   reg_controllable_hmaster1 =  controllable_hmaster1;
   reg_controllable_hmastlock =  controllable_hmastlock;
   reg_controllable_nstart =  controllable_nstart;
   reg_controllable_ndecide =  controllable_ndecide;
   reg_controllable_locked =  controllable_locked;
   reg_controllable_nhgrant0 =  controllable_nhgrant0;
   reg_controllable_hgrant1 =  controllable_hgrant1;
   reg_controllable_hgrant2 =  controllable_hgrant2;
   reg_controllable_hgrant3 =  controllable_hgrant3;
   reg_controllable_busreq =  controllable_busreq;

 end
endmodule

-------------------------------