amba3f9y.aag

aag 285 19 37 1 229
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40 1
42 30
44 16
46 434
48 457
50 472
52 18
54 474
56 493
58 36
60 499
62 2
64 28
66 10
68 4
70 500
72 509
74 512
76 514
78 38
80 32
82 518
84 529
86 8
88 530
90 6
92 26
94 538
96 546
98 558
100 568
102 127
104 22
106 34
108 24
110 570
112 20
398
114 22 3
116 26 5
118 117 115
120 32 7
122 121 118
124 102 40
126 125 122
128 104 40
130 58 40
132 131 128
134 132 39
136 134 19
138 21 16
140 29 6
142 28 7
144 143 141
146 145 138
148 21 17
150 29 2
152 28 3
154 153 151
156 155 148
158 20 17
160 29 4
162 28 5
164 163 161
166 165 158
168 106 40
170 42 40
172 171 138
174 170 139
176 175 173
178 52 40
180 178 9
182 179 8
184 183 181
186 184 176
188 78 40
190 188 148
192 189 149
194 193 191
196 108 40
198 197 158
200 196 159
202 201 199
204 202 194
206 204 186
208 207 168
210 48 40
212 56 40
214 213 211
216 60 40
218 217 214
220 72 40
222 221 168
224 222 218
226 224 11
228 86 40
230 229 8
232 228 9
234 233 231
236 234 10
238 44 40
240 239 17
242 238 16
244 243 241
246 112 40
248 247 21
250 246 20
252 251 249
254 253 245
256 254 236
258 257 227
260 259 209
262 260 167
264 262 157
266 264 147
268 266 137
270 131 129
272 270 39
274 272 18
276 275 268
278 92 40
280 278 131
282 280 24
284 282 19
286 285 276
288 279 131
290 288 24
292 290 18
294 293 286
296 80 40
298 296 131
300 298 30
302 300 19
304 303 294
306 297 131
308 306 30
310 308 18
312 311 304
314 189 38
316 188 39
318 317 315
320 319 130
322 321 312
324 196 25
326 197 24
328 327 325
330 329 130
332 331 322
334 170 31
336 171 30
338 337 335
340 339 130
342 341 332
344 178 19
346 179 18
348 347 345
350 349 130
352 351 342
354 74 40
356 24 5
358 356 354
360 359 352
362 82 40
364 30 7
366 364 362
368 367 360
370 69 63
372 370 91
374 373 40
376 375 131
378 376 38
380 379 368
382 96 40
384 94 40
386 385 383
388 98 40
390 389 386
392 100 40
394 392 391
396 395 380
398 397 126
400 46 40
402 401 220
404 70 40
406 405 219
408 407 403
410 149 2
412 110 40
414 413 410
416 415 408
418 159 4
420 54 40
422 421 418
424 423 416
426 139 6
428 88 40
430 429 426
432 431 424
434 433 403
436 11 8
438 436 15
440 438 218
442 440 12
444 442 35
446 217 34
448 447 211
450 446 210
452 451 449
454 452 215
456 455 445
458 50 40
460 459 35
462 84 40
464 76 40
466 465 462
468 467 461
470 469 433
472 470 461
474 433 423
476 442 34
478 212 210
480 478 217
482 480 34
484 483 212
486 213 210
488 486 446
490 489 485
492 490 477
494 214 34
496 495 216
498 497 483
500 433 407
502 220 28
504 221 13
506 504 438
508 507 503
510 355 24
512 511 5
514 470 467
516 363 30
518 517 7
520 463 8
522 15 13
524 522 520
526 462 28
528 527 525
530 433 431
532 468 384
534 469 385
536 535 533
538 536 433
540 533 382
542 532 383
544 543 541
546 545 433
548 384 382
550 548 468
552 551 388
554 550 389
556 555 553
558 557 433
560 550 388
562 561 392
564 560 393
566 565 563
568 567 433
570 433 415
i0 i_hbusreq0
i1 i_hbusreq1
i2 i_hbusreq2
i3 controllable_hmastlock
i4 controllable_nstart
i5 i_hburst1
i6 i_hburst0
i7 controllable_hmaster1
i8 controllable_locked
i9 controllable_hmaster0
i10 i_hlock0
i11 controllable_hgrant1
i12 i_hlock1
i13 controllable_busreq
i14 controllable_hgrant2
i15 i_hlock2
i16 i_hready
i17 controllable_ndecide
i18 controllable_nhgrant0
l0 n41
l1 reg_controllable_hgrant2_out
l2 reg_controllable_hmaster1_out
l3 sys_fair0done_out
l4 reg_stateG3_0_out
l5 env_fair1done_out
l6 reg_controllable_locked_out
l7 sys_fair3done_out
l8 reg_stateG3_1_out
l9 reg_controllable_ndecide_out
l10 reg_stateG3_2_out
l11 reg_i_hbusreq0_out
l12 reg_controllable_busreq_out
l13 reg_controllable_nstart_out
l14 reg_i_hbusreq1_out
l15 sys_fair1done_out
l16 reg_stateG2_out
l17 reg_stateG10_1_out
l18 env_fair0done_out
l19 reg_controllable_nhgrant0_out
l20 reg_i_hlock2_out
l21 reg_stateG10_2_out
l22 reg_stateA1_out
l23 reg_controllable_hmastlock_out
l24 sys_fair4done_out
l25 reg_i_hbusreq2_out
l26 reg_i_hlock1_out
l27 fair_cnt<0>_out
l28 fair_cnt<1>_out
l29 fair_cnt<2>_out
l30 fair_cnt<3>_out
l31 env_safe_err_happened_out
l32 reg_i_hlock0_out
l33 reg_i_hready_out
l34 reg_controllable_hgrant1_out
l35 sys_fair2done_out
l36 reg_controllable_hmaster0_out
o0 o_err
c
amba_3_new_9
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 amba3f9.v   ---gives--> amba3f9.mv
> abc -c "read_blif_mv amba3f9.mv; strash; refactor; rewrite; dfraig; rewrite; dfraig; write_aiger -s amba3f9y.aig"   ---gives--> amba3f9y.aig
> aigtoaig amba3f9y.aig amba3f9y.aag   ---gives--> amba3f9y.aag (this file)
Content of amba3f9.v:
module amba_3_new_9(
        o_err,
        i_clk,
        i_hready,
        i_hbusreq0,
        i_hlock0,
        i_hbusreq1,
        i_hlock1,
        i_hbusreq2,
        i_hlock2,
        i_hburst0,
        i_hburst1,
        controllable_hmaster0,
        controllable_hmaster1,
        controllable_hmastlock,
        controllable_nstart,
        controllable_ndecide,
        controllable_locked,
        controllable_nhgrant0,
        controllable_hgrant1,
        controllable_hgrant2,
        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_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_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_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_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 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 [3:0] fair_cnt;

wire env_safe_err0;
wire env_safe_err1;
wire env_safe_err2;
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_err;

wire env_fair0;
wire env_fair1;

wire sys_fair0;
wire sys_fair1;
wire sys_fair2;
wire sys_fair3;
wire sys_fair4;
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);

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

// =============================================================
//                        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)));

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

// G(((stateG2=1) * (start=1)) -> FALSE;
assign sys_safe_err4 =  ~( ~(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_err5 =  (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_err6 =  ~( ~(reg_i_hready) | ( ~reg_controllable_nhgrant0 ^~ ( ~(controllable_hmaster0) & ~(controllable_hmaster1) ) ) );

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

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

// HMASTLOCK:
// G(  (hready=1) -> (locked=0 <-> X(hmastlock=0) ) );
assign sys_safe_err9 =  ~( ~(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_err10 =  ~( ~(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_err11 =  ~( ~(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_err12 =  ~( ~(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_err13 =  ~( ~(controllable_nstart) | ( reg_controllable_hmastlock ^~ controllable_hmastlock) );

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

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

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

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

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

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

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

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

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

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

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

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

// default master
// G((decide=1  *  hbusreq0=0  *  hbusreq1=0  *  hbusreq2=0) -> X(hgrant0=1));
assign sys_safe_err26 =  ~( ~(~reg_controllable_ndecide & (~reg_i_hbusreq0 & ~reg_i_hbusreq1 & ~reg_i_hbusreq2)) | (~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;

// =============================================================
//                          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;

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);
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_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_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;
  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;
  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;
      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;
      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

   // 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_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_busreq =  controllable_busreq;

 end
endmodule

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