CELLTYPE "
CrossRAM"
PORTS [Vdd, Gnd, PadVdd, PadGnd, nPrecharge, Access, Write, Read<BOOL, Address<INT[11], Data=INT[32], Parity=INT[1]]
Expand
nPrechargeB, AccessB, WriteB, nWriteB, ReadB, nReadB: BOOL;
AddressB: INT[11];
AddressHigh: INT[3];
AddressLow: INT[8];
Select: INT[8];
Bit, nBit: BIT[264];
Words: INT[256];
PadI, DataI: INT[33];
EQUIVALENCE PadI, [Parity, Data];
EQUIVALENCE AddressB, [AddressHigh, AddressLow];
prechargePad: InputPad[Vdd: PadVdd, Gnd: PadGnd, Pad: nPrecharge, DataOut: nPrechargeB];
accessPad: InputPad[Vdd: PadVdd, Gnd: PadGnd, Pad: Access, DataOut: AccessB];
writePad: DifferentialInputPad[Vdd: PadVdd, Gnd: PadGnd, Pad: Write, DataOut: WriteB, nDataOut: nWriteB];
readPad: DifferentialInputPad[Vdd: PadVdd, Gnd: PadGnd, Pad: Read, DataOut: ReadB, nDataOut: nReadB];
addressPads: CrossAddressPads[Vdd: PadVdd, Gnd: PadGnd, Pad: Address, DataOut: AddressB];
dataPads: CrossDataPads[Vdd: PadVdd, Gnd: PadGnd, Read: ReadB, nRead: nReadB, Write: WriteB, nWrite: nWriteB, Pads: PadI, Data: DataI];
dataBuffer: CrossDataBuffer[Read: ReadB, nRead: nReadB, Write: WriteB, nWrite: nWriteB, Data: DataI, Select: Select, Bit: Bit, nBit: nBit];
decoder: CrossDecoder[Address: AddressLow, Access: AccessB, Words: Words];
demultiplexor: CrossDemultiplexor[Address: AddressHigh, Select: Select];
precharge: CrossPrecharge[nPrecharge: nPrechargeB, Bit: Bit, nBit: nBit];
ram: CrossRAMArray[Words: Words, Bit: Bit, nBit: nBit];
State
accessOccured, precharged: BOOL ← FALSE,
address: CARDINAL,
memory: SEQUENCE length: CARDINAL OF CrossRAMWord
Initializer
state: CrossRAMStateRef ← NEW [CrossRAMStateRec[2048]];
cell.realCellStuff.state ← state;
EvalSimple
IF NOT Vdd OR Gnd OR NOT PadVdd OR PadGnd THEN RoseTypes.Stop["Some power supply has incorrect value", $FailedAssertion];
IF (NOT nPrecharge AND Access) OR (Write AND Read) OR (NOT nPrecharge AND Write) THEN RoseTypes.Stop["Control lines used incorrectly", $FailedAssertion];
IF NOT nPrecharge THEN precharged ← TRUE;
drive[Data] ← ignore;
drive[Parity] ← ignore;
IF Access
THEN {
IF NOT precharged THEN RoseTypes.Stop["Access attempted without precharge", $FailedAssertion];
IF accessOccured AND address#Address THEN RoseTypes.Stop["Address may not change during access", $FailedAssertion];
accessOccured ← TRUE;
address ← Address;
IF Read
THEN {
Data ← memory[address].data;
drive[Data] ← drive;
Parity ← memory[address].parity;
drive[Parity] ← drive;
};
IF Write THEN {memory[address].data ← Data; memory[address].parity ← Parity};
};
IF NOT Access AND accessOccured THEN {accessOccured ← FALSE; precharged ← FALSE};
Test Write2Read2 BlackBox
AccessRAM:
PROC [write:
BOOL, address:
CARDINAL, data:
LONG
CARDINAL, parity:
CARDINAL] = {
d: BitOps.BitDWord ← BitOps.ILID[data, BitOps.BitDWordZero, 32, 0, 32];
Address ← address;
precharge
nPrecharge ← FALSE;
[] ← RoseRun.Eval[handle];
nPrecharge ← TRUE;
[] ← RoseRun.Eval[handle];
enable select line
Access ← TRUE;
if write then enable write drivers
IF write
THEN {
drive[Data] ← drive;
drive[Parity] ← drive;
Write ← TRUE;
}
ELSE {
drive[Data] ← test;
drive[Parity] ← test;
Read ← TRUE;
};
Data ← d;
Parity ← parity;
[] ← RoseRun.Eval[handle];
disable select line
Access ← Write ← Read ← FALSE;
drive[Data] ← ignore;
drive[Parity] ← ignore;
[] ← RoseRun.Eval[handle];
};
Vdd ← TRUE; Gnd ← FALSE; PadVdd ← TRUE; PadGnd ← FALSE;
drive[Vdd] ← drive; drive[Gnd] ← drive;
drive[PadVdd] ← drive; drive[PadGnd] ← drive;
nPrecharge ← TRUE; Access ← FALSE; Write ← FALSE; Read ← FALSE;
drive[nPrecharge] ← drive; drive[Access] ← drive;
drive[Write] ← drive; drive[Read] ← drive;
drive[Address] ← drive;
drive[Data] ← ignore; drive[Parity] ← ignore;
[] ← RoseRun.Eval[handle ! RoseTypes.Stop => IF data=$FailedAssertion THEN CONTINUE ];
AccessRAM[write: TRUE, address: 0, data: 0, parity: 0];
AccessRAM[write: TRUE, address: 1, data: LAST[LONG CARDINAL], parity: 1];
AccessRAM[write: FALSE, address: 0, data: 0, parity: 0];
AccessRAM[write: FALSE, address: 1, data: LAST[LONG CARDINAL], parity: 1];
ENDCELLTYPE