-- 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
(635)\168u8U14f3 1f0 31u8U25u8U51f3 1f0 42f3 1f0 62u6U7u4U5f3 1f0 28u2U7f3 1f0 1u4U1u2U5u3U3u6U10u4U16u4U9u4U12f3 1f0 30u6U10u4U17u4U9u4U13f3 1f0 1396f3 1f0 100u6U6u4U5f3 1f0 30u4U3f3 1f0 1f3 1f0 164u8U14f3 1f0 1u8U16u8U14f3 1f0 1u8U18u6U6u4U5f3 1f0 54u2U7f3 1f0 1u4U1u2U4u6U7u4U5f3 1f0 3u4U6u4U37u4U5f3 1f0 3u4U6u4U254f3 1f0 23f3 1f0
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
\64u8U12f3 1f0 1u8U14u8U12f3 1f0 1u8U17u6U6u4U4f3 1f0 3u4U5u4U22u4U4f3 1f0 3u4U5u4U
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

\64f3 1f0