-- FIFO.spec

FIFO DEFINITION = {
IN Init,
WriteRequest,
ReadRequest,
DataIn(16)
OUT SpaceAv,
DataAv,
DataOut(16)
STATE A(37,16), rp, wp
GUARDIAN
Init↑ onlywhen ~ReadRequest & ~WriteRequest,
ReadRequest↑ onlywhen DataAv,
WriteRequest↑ onlywhen SpaceAv
DATAFLOW
DataAv <= delay(~ReadRequest) & rp<wp,
SpaceAv <= delay(~WriteRequest) & wp<wp+size,
A[wp] <= DataIn,
DataOut <= A[rp]
CONTROL
repeat {
when Init↑ : rp := wp := 0;

on Init↑ ← exit in
par [ repeat {
when ReadRequest↑ : skip;
when ReadRequest↑ : rp := rp+1}
//
repeat {
when WriteRequest↑ : skip;
when WriteRequest↑ : wp := wp+1}
]
}
} -- end of FIFO DEFINITION

FIFO IMPLEMENTATION = {
COMPONENTS
w,r: PhaseSplitter,
ws, rs: CircularShifter(37),
inPass(37): PassTransistor,
data: DataArray(16, 37),
sa, da: AndOr(2, 37),
saAnd, daAnd: And,
saInhibit, daInhibit: Inhibitor,
dIn(37), sTemp, dTemp, siTemp, diTemp,
dw(37), dr(37), WR, WR’, RR, RR’: NODE
REPRESENTATION
Din0, Din1, Din2, Din3, Din4, Din5, Din6, Din7, Din8, Din9, Din10, Din11, Din12, Din13,
Din14, Din15 ALIAS DataIn,
Dout0, Dout1, Dout2, Dout3, Dout4, Dout5, Dout6, Dout7, Dout8, Dout9, Dout10, Dout11,
Dout12, Dout13, Dout14, Dout15 ALIAS DataIn
CONNECTIONS
w(in: WriteRequest, out1: WR’, out2: WR),
r(in: ReadRequest, out1: RR’, out2: RR),

ws(init(1..37): Init, inP1(1..37): WR, inP2(1..37): WR’, out: dw),
rs(init(1..37): Init, inP1(1..37): RR, inP2(1..37): RR’, out: dr),

inPass(i)(in: DataIn(i), out: dIn(i), switch: WR’) | i IN 1..37,
data(input: dIn, output: DataOut, write: dw, read: dr),

sa(in(1): dw, in(2, 1..36): dr(2..37), in(2, 37): dr(1), out: sTemp),
da(in(1): dw, in(2): dr, out: dTemp),

saAnd(in1: sTemp, in2: siTemp, out: SpaceAv),
daAnd(in1: dTemp, in2: diTemp, out: DataAv),

saInhibit(in1: WR, in2: WR’, out: siTemp),
daInhibit(in1: RR, in2: RR’, out: diTemp)
} -- end of FIFO

PassTransistor DEFINITION = {
IN in, switch
OUT out
DATAFLOW
out <= in & switch
} -- end of PassTransistor

PhaseSplitter DEFINITION = {
IN in
OUT out1, out2
CONTROL
repeat {
when in↑ ← out1 := lo; out2 := hi []
when in↑ ← out2 := lo; out1 := hi
}
} -- end of PhaseSplitter

CircularShifter(size) DEFINITION = {
INPUT: init, inP1, inP2
OUTPUT: out(size)
STATE i
GUARDIAN
inP1↑ onlywhen ~inP2,
inP1↑ onlywhen ~inP2,
inP2↑ onlywhen ~inP1,
inP2↑ onlywhen ~inP1
CONTROL
repeat {
when Init↑ : i := 0; out(0) := 1; out(1..size-1) := 0;

on Init↑ ← exit in
repeat {
when inP2↑ : skip;
when inP1↑ : out(i+1 MOD size) := 1;
when inP1↑ : skip;
when inP2↑ : out(i) := 0; i := i+1 MOD size}
}
} -- end of CircularShifter

DataArray(wordSize, columnSize) DEFINITION = {
IN in(wordSize), write(columnSize), read(columnSize)
OUT out(wordSize)
STATE A(1..wordSize, 1..columnSize)
DATAFLOW
A(i) <= in & write(i), out <= A(j) & read(j)
} -- end of DataArray

Inhibitor DEFINITION = {
IN in1, in2
OUT out
GUARDIAN
in1↑ onlywhen ~in2,
in1↑ onlywhen ~in2,
in2↑ onlywhen ~in1,
in2↑ onlywhen ~in1
CONTROL
repeat {
when in2↑ : skip;
when in1↑ : out := hi;
when in1↑ : skip;
when in2↑ : out := lo}
}
} -- end of Inhibitor

And DEFINITION = {
IN in1, in2
OUT out
DATAFLOW
out <= in1 & in2
} -- end of And

AndOr(NumAnd, NumOr) DEFINITION = {
IN in(NumAnd, NumOr)
OUT out
DATAFLOW
out <= Map(OR, i, 1, NumOr, Map(AND, j, 1, NumAnd, in(j, i)))
} -- end of AndOr