#include <gates.xtc>
 
/// Convert between Level and Transition style modelling

Event clk     // D-Type clk
 
// The models

Process Arbiter(Bool to, oi, go, ao, gi, oo, ti, ri, bool start) {
  Bool i2, i3, i4, i5, i6, ri'
 
  return DFF(ti, clk, to, start)*
         AND2(to, i2, i3)*
         OR2(i3, oi, oo)*
         OR2(i3, gi, i6)*
         AND2(ri, i6, ao)*
         INV(ri, ri')*
         AND2(ri', gi, go)*
         DFF(i4, clk, i2, false)*
         OR2(to, i2, i5)*
         AND2(ri, i5, i4)-(i2 i3 i4 i5 i6 ri')
}
 
Process GND(Bool a) {
  Process v(a)
  v <- a.0 v
  return v
}
 
Process Level2Sync(Bool l, Event e, clk) {
  Process S
  
  S <- (l.1 e) (l.1 clk) S + (l.0) (l.0 clk) S
  
  return S
  
}

/*
  Single arbiter test ---------------------------------------

Process Arb, ArbAndSync, ArbAndSyncOnly
Process HE1,HE2,HE3,HE4
Bool to, oi, go, ao, gi, oo, ti, ri;
Event R, A, T

Arb <- Arbiter(to, oi, go, ao, gi, oo, ti, ri, false) 
ArbAndSync <- Arb * Level2Sync(to,T,clk) * Level2Sync(ao,A,clk)

ArbAndSyncOnly <- ArbAndSync - (to oi go ao gi oo ti ri)


*/
/* Equivalent to arbiter and "T" sync
HE1 <- clk HE2
HE2 <- clk HE2 + T HE3
HE3 <- clk HE4
HE4 <- clk HE4 + T HE3

print may_eq(~ArbAndSyncOnly,HE1)

HE1 <- clk HE3 + A HE2
HE2 <- clk HE3
HE3 <- clk HE3 + A HE2 + T HE2 + (A T) HE2

print may_eq(~ArbAndSyncOnly,HE1)
*/

/* 
  Arbiter Loop Test ------------------------------------------
*/

n=5        // Number of Arbiters (>1)
tokp=0     // where to start token

Process As[n]
Bool t[n], oi[n], oo[n], a[n], r[n], invo, invi
 
Event R[n], A[n], T[n]

As[0] <- Arbiter(t[0], oi[0], oo[0], a[0], invo, invi,
                t[n-1], r[0], (tokp==0))*
                Level2Sync(t[0], T[0], clk)*
                Level2Sync(a[0], A[0], clk)*
                Level2Sync(r[0], R[0], clk)
 
for (i=1;i<n;i++)
  As[i] <- Arbiter(t[i], oi[i], oo[i], a[i], oo[i-1], oi[i-1],
                  t[i-1], r[i], (tokp==i))*
                  Level2Sync(t[i], T[i], clk)*
                  Level2Sync(a[i], A[i], clk)*
                  Level2Sync(r[i], R[i], clk)
 
Process CONS

Process Arb

/* Test for Token Circulation -------------------------------------------
*/

Arb <- ((*As)*GND(oi[n-1])*INV(invi, invo)-
       ((*oi) (*oo) invo invi (*t) (*a) (*r) clk (*A) (*R)))

//display ~Arb

Process TokCirc[n]

for(int i=0;i < n-1;i++)
  TokCirc[i] <- (T[i]) TokCirc[i+1]
TokCirc[n-1] <- (T[n-1]) TokCirc[0]

print "Arb > TokCirc : " 
print (~Arb > TokCirc[0])
print "\n"

/*
  Requests high test ------------------------------------------

Arb <- ~((*As)*GND(oi[n-1])*INV(invi, invo)-
        ((*oi) (*oo) invo invi (*t) (*a) (*r) clk))

Process Test, Cons, tmp

Event sync

Test <- ((*R) sync) Test

tmp = NullP

for (i=0;i<n;i++)
  tmp = tmp + (T[i] sync) Cons
  
Cons <- tmp

Process RequestsHigh

RequestsHigh <- Test*Cons*Arb-((*R) sync)

//display ~RequestsHigh

Process AckCirc[2*n]

for(int i=0;i < n;i++)
  AckCirc[i] <- (A[0] T[i]) AckCirc[i+1]
for(int i=0;i < n-1;i++)
  AckCirc[i+n] <- (A[i] T[i]) AckCirc[i+n+1]
AckCirc[2*n - 1] <- (A[n-1] T[n-1]) AckCirc[n]


print "RequestsHigh > AckCirc : " 
print (~RequestsHigh > AckCirc[0])
print "\n"

*/