Imports BitOps, BitSwOps, Dragon;
Open BitOps, BitSwOps, Dragon;

Cedar
memBits: TYPE = ARRAY [0..5) OF BitWord;
;

CacheEntry: CELL[

Vdd, Gnd<BOOL,
PhAb, PhBb, nPhBb<BOOL,
Resetb<BOOL, 
VirtualPage, nVirtualPage<INT[24],
VirtualBlock, nVirtualBlock<INT[6],
RealPage, nRealPage<INT[24],
RealBlock, nRealBlock<INT[6],
CAMPageAccess, nCAMPageAccess=SWITCH[24]-S-X,
CAMBlockAccess, nCAMBlockAccess=SWITCH[6]-S-X,

PBits, nPBits=SWITCH[66]-S-X,
MBits, nMBits=SWITCH[66]-S-X,

nVirtualMatch, nMatchPageClean, nMatchCellShared=BOOL,
nMapValid, nRealMatch, nVictimClean=BOOL,
nMatchTIP=BOOL,
CellAdr, nCellAdr<INT[8],
VirtualAccess, nVirtualAccess, SelCell, SelVictimAdr, SelMapAdr, SelRealData, SelPageFlag, SelVictimData, SelRealAdr<BOOL,
FinishSharedStore<BOOL,
VPValid, nVPValid, RPValid, nRPValid, RPDirty, nRPDirty, Master, nMaster, Shared, nShared, Victim, nVictim, TIP, nTIP, Broken, nBroken=BIT-S-X,
MAdrLow, nMAdrLow<BOOL,
PAdrLow, nPAdrLow<BOOL,
PStore<BOOL,
VictimFeedback, nVictimFeedback, ShiftVictim, nShiftVictim<BOOL,
ForceDataSelect<BOOL,

VictimIn<BOOL,
VictimOut>BOOL
]

InitData
cellNumber: BitWord
State
vpValid, nvpValid: BOOL,
rpValid, nrpValid: BOOL,
rpDirty, nrpDirty: BOOL,
master, nmaster: BOOL,
shared, nshared: BOOL,
victim, nvictim: BOOL,
tip, ntip: BOOL,
broken, nbroken: BOOL,
hexVirtualPage, hexRealPage, hexBlock: HexWord,
words: ARRAY [0..4) OF HexWord,
parity: ARRAY [0..4) OF BOOL,
virtualPage, nvirtualPage: BitDWord,
realPage, nrealPage: BitDWord,
block, nblock: BitWord,
data: ARRAY [0..2) OF ARRAY BOOLEAN OF memBits,
vpMatch, vblMatch, rpMatch, rblMatch: BOOL,
selVMap, vSelCell, selRMap, rSelCell: BOOL,
decodeSelect, victimAdrSelect, victimDataSelect, victimFlagSelect: BOOL,
realMatchSelect, dataSelect, addressSelect, virtualDataSelect: BOOL,
thisCellAdr: BitWord
Initializer
thisCellAdr _ cellNumber;
EvalSimple
oldMemBits: ARRAY [0..2) OF memBits;

RWB: PROC [access: BOOL, bus, nBus: Switch, bit, nbit: BOOL] RETURNS [newBus, nNewBus: Switch, newBit, newnBit: BOOL] = {
s: SwitchTypes.Strength _ IF access THEN drive ELSE none;
IF access THEN {
bit _ (NOT nbit) AND bus.val=H;
nbit _ (NOT bit) AND nBus.val=H;
bit _ (NOT nbit) AND bus.val=H;
};
nNewBus _ SIBISS[bit, nBus, [[none, X], [s, L]]];
newBus _ SIBISS[nbit, bus, [[none, X], [s, L]]];
newBit _ bit;
newnBit _ nbit;
};

RWW: PROC [access: BOOL, busD, nBusD: SwitchMWord, field, nfield: BitWord, fieldWidth: CARDINAL] RETURNS [newField, newnField: BitWord] = TRUSTED {
s: SwitchTypes.Strength _ IF access THEN drive ELSE none;
IF access THEN FOR i:CARDINAL IN [0..fieldWidth) DO
field _ IBIW[(NOT EBFW[nfield, fieldWidth, i]) AND busD[i].val=H, field, fieldWidth, i];
nfield _ IBIW[(NOT EBFW[field, fieldWidth, i]) AND nBusD[i].val=H, nfield, fieldWidth, i];
field _ IBIW[(NOT EBFW[nfield, fieldWidth, i]) AND busD[i].val=H, field, fieldWidth, i];
ENDLOOP;
SCWTS[field, fieldWidth, 0, fieldWidth, nBusD, fieldWidth, 0, fieldWidth, [[none, X], [s, L]]];
SCWTS[nfield, fieldWidth, 0, fieldWidth, busD, fieldWidth, 0, fieldWidth, [[none, X], [s, L]]];
newField _ field;
newnField _ nfield;
};

RWD: PROC [access: BOOL, busD, nBusD: SwitchMWord, field, nfield: BitDWord, fieldWidth: CARDINAL] RETURNS [newField, newnField: BitDWord] = TRUSTED {
s: SwitchTypes.Strength _ IF access THEN drive ELSE none;
IF access THEN FOR i:CARDINAL IN [0..fieldWidth) DO
field _ IBID[(NOT EBFD[nfield, fieldWidth, i]) AND busD[i].val=H, field, fieldWidth, i];
nfield _ IBID[(NOT EBFD[field, fieldWidth, i]) AND nBusD[i].val=H, nfield, fieldWidth, i];
field _ IBID[(NOT EBFD[nfield, fieldWidth, i]) AND busD[i].val=H, field, fieldWidth, i];
ENDLOOP;
SCDTS[field, fieldWidth, 0, fieldWidth, nBusD, fieldWidth, 0, fieldWidth, [[none, X], [s, L]]];
SCDTS[nfield, fieldWidth, 0, fieldWidth, busD, fieldWidth, 0, fieldWidth, [[none, X], [s, L]]];
newField _ field;
newnField _ nfield;
};

RWM: PROC [access: BOOL, busD, nBusD: SwitchMWord, field, nfield: BitMWord, fieldWidth: CARDINAL] = TRUSTED {
s: SwitchTypes.Strength _ IF access THEN drive ELSE none;
IF access THEN FOR i:CARDINAL IN [0..fieldWidth) DO
IBIM[(NOT EBFM[nfield, fieldWidth, i]) AND busD[i].val=H, field, fieldWidth, i];
IBIM[(NOT EBFM[field, fieldWidth, i]) AND nBusD[i].val=H, nfield, fieldWidth, i];
IBIM[(NOT EBFM[nfield, fieldWidth, i]) AND busD[i].val=H, field, fieldWidth, i];
ENDLOOP;
SCMTS[field, fieldWidth, 0, fieldWidth, nBusD, fieldWidth, 0, fieldWidth, [[none, X], [s, L]]];
SCMTS[nfield, fieldWidth, 0, fieldWidth, busD, fieldWidth, 0, fieldWidth, [[none, X], [s, L]]];
};

Assert[NOT MoreThanOneOf[PAdrLow, nPAdrLow]];
Assert[NOT MoreThanOneOf[MAdrLow, nMAdrLow]];
Assert[MAdrLow OR nMAdrLow];
Assert[NOT MoreThanOneOf[VictimFeedback, ShiftVictim]];
Assert[NOT MoreThanOneOf[VictimFeedback, nVictimFeedback]];
Assert[NOT MoreThanOneOf[ShiftVictim, nShiftVictim]];
Assert[NOT MoreThanOneOf[ShiftVictim, PhBb]];

FOR i:[0..2) IN [0..2) DO
oldMemBits[i] _ data[i][TRUE];
ENDLOOP;

vpMatch _ DAND[nVirtualPage, virtualPage]=BitDWordZero AND DAND[nvirtualPage, VirtualPage]=BitDWordZero;
vblMatch _ WAND[nVirtualBlock, block]=0 AND WAND[nblock, VirtualBlock]=0;
rpMatch _ DAND[nRealPage, realPage]=BitDWordZero AND DAND[nrealPage, RealPage]=BitDWordZero;
rblMatch _ WAND[nRealBlock, block]=0 AND WAND[nblock, RealBlock]=0;
selVMap _ NOT broken AND vpValid AND vpMatch;
vSelCell _ selVMap AND vblMatch;
selRMap _ NOT broken AND rpValid AND rpMatch;
rSelCell _ selRMap AND rblMatch;
IF selVMap AND PhBb THEN {
nMapValid _ FALSE;
IF nrpDirty THEN nMatchPageClean _ FALSE;
};
IF rSelCell AND PhBb THEN nRealMatch _ FALSE;
decodeSelect _ SelCell AND CellAdr=thisCellAdr AND CellAdr=WNOT[nCellAdr, 8];
victimAdrSelect _ SelVictimAdr AND victim;
victimDataSelect _ SelVictimData AND victim;
realMatchSelect _ SelRealData AND rSelCell;
IF NOT PhAb THEN dataSelect _ FALSE;
IF decodeSelect OR realMatchSelect OR victimDataSelect OR ForceDataSelect THEN dataSelect _ TRUE;
IF NOT PhAb THEN victimFlagSelect _ FALSE;
IF decodeSelect OR ForceDataSelect THEN victimFlagSelect _ TRUE;
IF NOT PhAb THEN addressSelect _ FALSE;
IF decodeSelect OR victimAdrSelect THEN addressSelect _ TRUE;
IF PhBb AND vSelCell THEN {
nVirtualMatch _ FALSE;
IF PStore AND rpDirty AND (nshared OR FinishSharedStore) THEN {master _ TRUE; nmaster _ FALSE};
IF shared THEN nMatchCellShared _ FALSE;
IF tip THEN nMatchTIP _ FALSE;
};
TRUSTED {
busD: SwitchMWord _ DESCRIPTOR[PBits];
nBusD: SwitchMWord _ DESCRIPTOR[nPBits];
access: BOOL _ PhBb AND vSelCell AND (NOT (PStore AND (nrpDirty OR (shared AND NOT FinishSharedStore))));
IF NOT PAdrLow THEN {  -- mumbo jumbo to ensure that at least one of these if clauses executes so that the instructions get updated
dataFD: BitMWord _ DESCRIPTOR[data[0][FALSE]];
dataTD: BitMWord _ DESCRIPTOR[data[0][TRUE]];
RWM[access AND nPAdrLow, busD, nBusD, dataTD, dataFD, 66];
};
IF PAdrLow THEN {
dataFD: BitMWord _ DESCRIPTOR[data[1][FALSE]];
dataTD: BitMWord _ DESCRIPTOR[data[1][TRUE]];
RWM[access, busD, nBusD, dataTD, dataFD, 66];
};
};
TRUSTED {
busD: SwitchMWord _ DESCRIPTOR[MBits];
nBusD: SwitchMWord _ DESCRIPTOR[nMBits];
access: BOOL _ dataSelect;
IF nMAdrLow THEN {
dataFD: BitMWord _ DESCRIPTOR[data[0][FALSE]];
dataTD: BitMWord _ DESCRIPTOR[data[0][TRUE]];
RWM[access, busD, nBusD, dataTD, dataFD, 66];
};
IF MAdrLow THEN {
dataFD: BitMWord _ DESCRIPTOR[data[1][FALSE]];
dataTD: BitMWord _ DESCRIPTOR[data[1][TRUE]];
RWM[access, busD, nBusD, dataTD, dataFD, 66];
};
[RPValid, nRPValid, rpValid, nrpValid] _ RWB[access, RPValid, nRPValid, rpValid, nrpValid];
[Master, nMaster, master, nmaster] _ RWB[access, Master, nMaster, master, nmaster];
[Shared, nShared, shared, nshared] _ RWB[access, Shared, nShared, shared, nshared];
[TIP, nTIP, tip, ntip] _ RWB[access, TIP, nTIP, tip, ntip];
[Broken, nBroken, broken, nbroken] _ RWB[access, Broken, nBroken, broken, nbroken];
};
{
access: BOOL _ victimFlagSelect;
[Victim, nVictim, victim, nvictim] _ RWB[access AND NOT (thisCellAdr=0 AND Resetb), Victim, nVictim, victim, nvictim];
};
{
access: BOOL _ dataSelect OR (SelPageFlag AND selRMap);
[VPValid, nVPValid, vpValid, nvpValid] _ RWB[access, VPValid, nVPValid, vpValid, nvpValid];
[RPDirty, nRPDirty, rpDirty, nrpDirty] _ RWB[access, RPDirty, nRPDirty, rpDirty, nrpDirty];
};
TRUSTED {
busD: SwitchMWord _ DESCRIPTOR[CAMPageAccess];
nBusD: SwitchMWord _ DESCRIPTOR[nCAMPageAccess];
[virtualPage, nvirtualPage] _ RWD[(addressSelect AND VirtualAccess) OR (rSelCell AND SelRealAdr), busD, nBusD, virtualPage, nvirtualPage, 24];
};
TRUSTED {
busD: SwitchMWord _ DESCRIPTOR[CAMPageAccess];
nBusD: SwitchMWord _ DESCRIPTOR[nCAMPageAccess];
[realPage, nrealPage] _ RWD[(addressSelect AND nVirtualAccess) OR (selVMap AND SelMapAdr), busD, nBusD, realPage, nrealPage, 24];
};
TRUSTED {
busD: SwitchMWord _ DESCRIPTOR[CAMBlockAccess];
nBusD: SwitchMWord _ DESCRIPTOR[nCAMBlockAccess];
[block, nblock] _ RWW[addressSelect, busD, nBusD, block, nblock, 6];
};
IF ShiftVictim THEN nvictim _ NOT VictimIn;
IF VictimFeedback THEN nvictim _ NOT victim;
IF PhBb THEN victim _ NOT nvictim;  -- this is where nPhBb is used
VictimOut _ IF broken THEN VictimIn ELSE victim;
IF victim AND nmaster AND PhBb THEN nVictimClean _ FALSE;
IF thisCellAdr=0 AND Resetb THEN {
victim _ TRUE;
nvictim _ FALSE;
}; 
hexVirtualPage _ ELFD[virtualPage, 24, 0, 24];
hexRealPage _ ELFD[realPage, 24, 0, 24];
hexBlock _ ELFW[block, 6, 0, 6];
TRUSTED {
assembleWord: BitDWord;
diff: BOOL _ FALSE;
FOR i:[0..2) IN [0..2) DO
IF oldMemBits[i]#data[i][TRUE] THEN {diff _ TRUE; EXIT};
ENDLOOP;
IF diff OR Resetb THEN FOR k:[0..2) IN [0..2) DO
FOR j:[0..2) IN [0..2) DO
desc: BitMWord _ DESCRIPTOR[data[j][TRUE]];
FOR i:[0..32) IN [0..32) DO
assembleWord _ IBID[EBFM[desc, 66, (2*i)+k], assembleWord, 32, i];
ENDLOOP;
words[2*k+j] _ ELFD[assembleWord, 32, 0, 32];
parity[2*k+j] _ EBFM[desc, 66, 64+k];
ENDLOOP;
ENDLOOP;
}
ENDCELL


ÌCacheEntry.rose
Last edited by: Barth, May 22, 1984 8:16:56 pm PDT
Timing and housekeeping interface

Buffered timing and housekeeping interface

CAM interface
RAM access
Cell control
Victim shift
�Ê­˜Jš
œ™Jš
œ2™2J˜Jš
œ!˜!Jš
œ˜J˜˜Jšœ	Ïkœ�œ�œ	˜(—J˜
J˜šœ�œ
˜J˜š
œ!™!Jšœ	�œ
˜—J™š
œ*™*Jšœ�œ
˜Jšœ�œ˜
—J™š
œ
™
Jšœ�œ˜"Jšœ�œ˜#Jšœ�œ˜Jšœ�œ˜Jšœ�œ�œ
˜-Jšœ �œ�œ
˜.—J˜™
Jšœ�œ�œ
˜Jšœ�œ�œ
˜—J˜™Jšœ1�œ
˜6Jšœ$�œ
˜)Jšœ
�œ
˜Jšœ�œ˜Jšœu�œ
˜zJšœ�œ
˜Jšœl�œ�œ
�œ
˜�
Jšœ�œ
˜Jšœ�œ
˜Jšœ�œ
˜Jšœ;�œ
˜@Jšœ�œ
˜—J˜™Jšœ	�œ
˜Jšœ
�˜—Jš
œ
˜
J˜˜J˜—˜Jšœ�œ
˜Jšœ�œ
˜Jšœ�œ
˜Jšœ�œ
˜Jšœ�œ
˜Jšœ�œ
˜Jšœ�œ
˜Jšœ�œ
˜J˜/Jšœ�œ�œ	˜Jšœ�œ�œ
�œ
˜Jš
œ$˜$Jš
œ˜Jš
œ˜Jšœ�œ�œ
�œ
�œ
�œ	˜/Jšœ&�œ
˜+Jšœ&�œ
˜+JšœC�œ
˜HJšœ?�œ
˜DJš
œ˜—š
œ˜J˜—˜
Jšœ�œ�œ	˜$J˜š�œ�œ
�œ �œ�œ,�œ˜yJšœ�œ�œ�œ˜9š�œ�œ˜Jšœ�œ�œ	�
œ
˜Jšœ�œ�œ
�
œ
˜ Jšœ�œ�œ	�
œ
˜Jš
œ˜—Jšœ�	œ�
œ�
œ˜1Jšœ�	œ�
œ�
œ˜0Jš
œ
˜
Jš
œ˜J˜J˜—š�œ�œ
�œ@�œ�œ"�œ˜“
Jšœ�œ�œ�œ˜9š�œ�œ
�œ�œ
�œ�˜3Jšœ�œ�œ
�œ�œ
�
œ˜XJšœ	�œ�œ
�œ�œ�
œ˜ZJšœ�œ�œ
�œ�œ
�
œ˜XJš�œ
˜—Jš�œM�
œ�
œ˜_Jš�œM�
œ�
œ˜_Jš
œ˜Jš
œ˜J˜J˜—š�œ�œ
�œA�œ�œ#�œ˜•
Jšœ�œ�œ�œ˜9š�œ�œ
�œ�œ
�œ�˜3Jšœ�œ�œ
�œ�œ
�
œ˜XJšœ	�œ�œ
�œ�œ�
œ˜ZJšœ�œ�œ
�œ�œ
�
œ˜XJš�œ
˜—Jš�œM�
œ�
œ˜_Jš�œM�
œ�
œ˜_Jš
œ˜Jš
œ˜J˜J˜—š
�œ�œ
�œA�œ�œ˜mJšœ�œ�œ�œ˜9š�œ�œ
�œ�œ
�œ�˜3Jš
�œ�œ
�œ�œ
�
œ˜PJš
�œ�œ
�œ�œ�
œ˜QJš
�œ�œ
�œ�œ
�
œ˜PJš�œ
˜—Jš�œM�
œ�
œ˜_Jš�œM�
œ�
œ˜_J˜J˜—Jšœ�œ#˜-Jšœ�œ#˜-Jšœ�œ˜Jšœ�œ-˜7Jšœ�œ1˜;Jšœ�œ+˜5Jšœ�œ#˜-J˜š�œ
�œ�˜Jšœ�œ˜Jš�œ
˜—J˜Jšœ
�œ)�œ
�œ)˜hJšœ�œ�œ
�œ˜IJšœ
�œ#�œ
�œ#˜\Jšœ�œ�œ
�œ˜CJšœ
�œ�œ	�œ	˜-Jšœ�œ
˜ Jšœ
�œ�œ	�œ	˜-Jšœ�œ
˜ š�œ	�œ�œ˜Jšœ�œ
˜Jš�œ
�œ�œ
˜)J˜—Jš�œ
�œ�œ�œ
˜-Jšœ�œ�œ	�œ˜MJšœ�œ˜*Jšœ!�œ˜,Jšœ�œ
˜+Jš�œ
�œ�œ�œ
˜$Jš�œ�œ�œ�œ�œ�œ
˜aJš�œ
�œ�œ�œ
˜*Jš�œ�œ�œ�œ
˜@Jš�œ
�œ�œ�œ
˜'Jš�œ�œ�œ�œ
˜=š�œ�œ
�œ˜Jšœ�œ
˜Jš�œ�œ	�œ
�œ�œ�œ�œ˜_Jš�œ�œ�œ
˜(Jš�œ�œ
�œ
˜Jš
œ˜—š�œ˜	Jšœ�
œ˜&Jšœ�
œ	˜(Jšœ�œ�œ
�œ
�œ	�œ�œ	�œ
�œ˜iš�œ
�œ	�œÏcl˜ƒ
Jšœ�
œ	�œ˜.Jšœ�
œ	�œ˜-Jš�œ�œ,˜:J˜—š�œ	�œ˜Jšœ�
œ	�œ˜.Jšœ�
œ	�œ˜-Jš�œ*˜-J˜—Jš
œ˜—š�œ˜	Jšœ�
œ˜&Jšœ�
œ	˜(Jšœ�œ˜š�œ
�œ˜Jšœ�
œ	�œ˜.Jšœ�
œ	�œ˜-Jš�œ*˜-J˜—š�œ	�œ˜Jšœ�
œ	�œ˜.Jšœ�
œ	�œ˜-Jš�œ*˜-J˜—Jšœ)�œ/˜[Jšœ%�œ+˜SJšœ%�œ+˜SJšœ�œ˜;Jšœ%�œ+˜SJ˜—˜
Jšœ�œ˜ Jš	œ%�œ�œ
�œ�œ,˜vJ˜—˜
Jšœ�œ�œ�œ
˜7Jšœ)�œ/˜[Jšœ)�œ/˜[J˜—š�œ˜	Jšœ�
œ˜.Jšœ�
œ˜0Jš	œ�œ�œ�œ�œ:˜Ž
J˜—š�œ˜	Jšœ�
œ˜.Jšœ�
œ˜0Jš	œ�œ�œ�œ
�œ3˜�
J˜—š�œ˜	Jšœ�
œ˜/Jšœ�
œ˜1Jšœ�œ/˜DJ˜—Jš�œ
�œ�œ
˜+Jš�œ�œ�œ˜,Jš�œ�œ
�œž˜BJšœ	�œ�œ
�œ˜0Jš
�œ�œ	�œ�œ�œ
˜9š�œ�œ�œ˜"Jšœ	�œ
˜Jšœ
�œ
˜J˜—Jšœ�œ˜.Jšœ�œ˜(Jšœ�œ˜ š�œ˜	J˜Jšœ�œ�œ
˜š�œ
�œ�˜Jš
�œ�œ�œ	�œ�œ˜8Jš�œ
˜—š�œ�œ�œ
�œ
�œ�˜0š�œ
�œ�˜Jšœ�
œ	�œ˜+š�œ�œ	�˜Jšœ�œ
�œ*˜BJš�œ
˜—Jšœ�œ˜-Jšœ�œ˜%Jš�œ
˜—Jš�œ
˜—J˜
——Jš
�˜—J˜J˜—…—&~3÷