amba4b9y.aag

aag 350 22 42 1 286
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 534
54 36
56 536
58 559
60 598
62 20
64 600
66 619
68 42
70 625
72 2
74 30
76 12
78 4
80 38
82 626
84 635
86 638
88 640
90 44
92 34
94 644
96 655
98 8
100 656
102 6
104 28
106 660
108 668
110 676
112 688
114 698
116 10
118 147
120 24
122 40
124 26
126 22
128 700
490
130 24 3
132 28 5
134 133 131
136 34 7
138 137 134
140 38 11
142 141 138
144 118 46
146 145 142
148 98 46
150 149 8
152 148 9
154 153 151
156 155 12
158 23 19
160 31 2
162 30 3
164 163 161
166 165 158
168 22 19
170 31 4
172 30 5
174 173 171
176 175 168
178 177 167
180 23 18
182 31 6
184 30 7
186 185 183
188 187 180
190 22 18
192 31 10
194 30 11
196 195 193
198 197 190
200 199 189
202 122 46
204 54 46
206 205 190
208 204 191
210 209 207
212 62 46
214 212 9
216 213 8
218 217 215
220 218 210
222 48 46
224 223 180
226 222 181
228 227 225
230 90 46
232 230 158
234 231 159
236 235 233
238 124 46
240 239 168
242 238 169
244 243 241
246 244 236
248 246 228
250 248 220
252 251 202
254 58 46
256 66 46
258 257 255
260 70 46
262 261 258
264 84 46
266 265 202
268 266 262
270 268 13
272 126 46
274 50 46
276 274 272
278 277 190
280 276 191
282 281 279
284 282 12
286 275 19
288 274 18
290 289 287
292 273 23
294 272 22
296 295 293
298 297 291
300 298 284
302 301 271
304 303 253
306 304 200
308 306 178
310 308 157
312 120 46
314 68 46
316 315 312
318 316 45
320 318 21
322 321 310
324 315 313
326 324 45
328 326 20
330 329 322
332 104 46
334 332 315
336 334 26
338 336 21
340 339 330
342 333 315
344 342 26
346 344 20
348 347 340
350 92 46
352 350 315
354 352 32
356 354 21
358 357 348
360 351 315
362 360 32
364 362 20
366 365 358
368 80 46
370 368 315
372 370 36
374 372 21
376 375 366
378 369 315
380 378 36
382 380 20
384 383 376
386 231 44
388 230 45
390 389 387
392 391 314
394 393 384
396 238 27
398 239 26
400 399 397
402 401 314
404 403 394
406 222 33
408 223 32
410 409 407
412 411 314
414 413 404
416 204 37
418 205 36
420 419 417
422 421 314
424 423 414
426 212 21
428 213 20
430 429 427
432 431 314
434 433 424
436 86 46
438 26 5
440 438 436
442 441 434
444 94 46
446 32 7
448 446 444
450 449 442
452 106 46
454 36 11
456 454 452
458 457 450
460 79 73
462 117 103
464 462 460
466 465 46
468 467 315
470 468 44
472 471 458
474 110 46
476 108 46
478 477 475
480 112 46
482 481 478
484 114 46
486 484 483
488 487 472
490 489 146
492 52 46
494 191 10
496 494 493
498 56 46
500 499 264
502 82 46
504 503 263
506 505 501
508 159 2
510 128 46
512 511 508
514 513 506
516 169 4
518 64 46
520 519 516
522 521 514
524 181 6
526 100 46
528 527 524
530 529 522
532 530 497
534 533 497
536 533 501
538 13 8
540 538 17
542 540 262
544 542 14
546 544 41
548 261 40
550 549 255
552 548 254
554 553 551
556 554 259
558 557 547
560 60 46
562 561 41
564 499 265
566 503 262
568 567 565
570 511 509
572 571 568
574 519 517
576 575 572
578 527 525
580 579 576
582 495 493
584 583 580
586 584 533
588 96 46
590 88 46
592 591 588
594 593 563
596 595 586
598 596 563
600 533 521
602 544 40
604 256 254
606 604 261
608 606 40
610 609 256
612 257 254
614 612 548
616 615 611
618 616 603
620 258 40
622 621 260
624 623 609
626 533 505
628 264 30
630 265 15
632 630 540
634 633 629
636 437 26
638 637 5
640 596 593
642 445 32
644 643 7
646 589 8
648 17 15
650 648 646
652 588 30
654 653 651
656 533 529
658 453 36
660 659 11
662 594 476
664 595 477
666 665 663
668 666 586
670 663 474
672 662 475
674 673 671
676 675 586
678 476 474
680 678 594
682 681 480
684 680 481
686 685 683
688 687 586
690 680 480
692 691 484
694 690 485
696 695 693
698 697 586
700 533 513
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 reg_i_hbusreq3_out
l36 env_safe_err_happened_out
l37 reg_i_hlock0_out
l38 reg_i_hready_out
l39 reg_controllable_hgrant1_out
l40 reg_controllable_hmaster0_out
l41 sys_fair2done_out
o0 o_err
c
amba_4_new_9
This file was written by ABC on Sat Aug 31 20:24:48 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 amba4b9.v   ---gives--> amba4b9.mv
> abc -c "read_blif_mv amba4b9.mv; strash; refactor; rewrite; dfraig; rewrite; dfraig; write_aiger -s amba4b9y.aig"   ---gives--> amba4b9y.aig
> aigtoaig amba4b9y.aig amba4b9y.aag   ---gives--> amba4b9y.aag (this file)
Content of amba4b9.v:
module amba_4_new_9(
        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 [3: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 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);

// 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 progress_in_sys_fair = (~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 >= 4'b1001);

// 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
      if(progress_in_sys_fair)
       begin
         env_fair0done = 0;
         env_fair1done = 0;
         fair_cnt = 0;
         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;
       end
      else
       begin
         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
    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

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