Page Numbers: No

-- FIFO.spec

FIFO DEFINITION = {
IN Init,
WriteRequest,
ReadRequest,
DataIn(16)
OUT SpaceAv,
DataAv,
DataOut(16)
GUARDIAN
{Initialized: BOOLEAN := false;
repeat {
when Init↑ ← if ReadRequest V WriteRequest then error;
Initialized := true ||
when ReadRequest↑ ← if ~Initialized V Init V ~DataAv
then error ||
when WriteRequest↑ ← if ~Initialized V Init V ~SpaceAv
then error
}
}
STATE A(37,16), rp, wp
DATAFLOW
DataAv <= ~ReadRequest & rp<wp,
SpaceAv <= ~WriteRequest & wp<wp+size,
A[wp] <= DataIn,
DataOut <= A[rp]
CONTROL
repeat {
when Init↑ ← rp := wp := 0;

quiton Init↑ in
par { repeat {
when ReadRequest↑ : rp := rp+1}
//
repeat {
when WriteRequest↑ : wp := wp+1}
}
}
} -- end of FIFO DEFINITION

FIFO IMPLEMENTATION = {
IN Init,
WriteRequest,
ReadRequest,
DataIn(16)
OUT SpaceAv,
DataAv,
DataOut(16)
COMPONENTS
w,r: PhaseSplitter,
ws, rs: CircularShifter(37),
data: DataArray(16, 37),
sa, da: AndOr(2, 37),
saAnd, daAnd: And,
saInhibit, daInhibit: Inhibitor,
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
(out1: WR’, out2: WR) ← w(in: WriteRequest),
(out1: RR’, out2: RR) ← r(in: ReadRequest),

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

(out: DataOut) ← data(in: dIn, switch: WF’, write: dw, read: dr),

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

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

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

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 inP1↑ : out(i+1 MOD size) := 1;
when inP2↑ : out(i) := 0; i := i+1 MOD size}
}
} -- end of CircularShifter

DataArray(wordSize, columnSize) DEFINITION = {
IN in(wordSize), switch, write(columnSize), read(columnSize)
OUT out(wordSize)
STATE A(1..wordSize, 1..columnSize)
DATAFLOW
A(i) <= in & write(i), out <= A(j) & read(j)
CONTROL
repeat {
when switch↑: A(i) <= in & write(i)}
} -- 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 in1↑ : out := hi;
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