Cell control
nVQMatchB, nQuadSharedB>BOOL,
QValidA, nQValidA, QSharedA, nQSharedA, QMasterA, nQMasterA=BIT-(Special XPhobic),
MQSelBA, MatchQSelBA<INT[4], nRQMatchA>BOOL, FinishSharedStoreAB<BOOL, nQDirtyB>INT[4],
PStoreAB, nPStoreAB<BOOL, PQSelAB<INT[4],
nPageDirtyB, nMapValidB>BOOL,
RPValidBitA, nRPValidBitA, RPDirtyBitA, nRPDirtyBitA, VPValidBitA, nVPValidBitA=BIT-(Special XPhobic),
ForceAllDataSelectsBA<BOOL, nRealBlockMatchA, nVirtualBlockMatchB>BOOL,
CellAdrBA, nCellAdrBA<INT[7],
SenseRMatchB, SenseVictimA, SelOrphanAdrBA, SelMapAdrBA, SelVPBA, SelRPVictimBA, SelRPDecoderBA, SelRealDataBA, SelPageFlagsBA, SelDecodeBA<BOOL,
SenseVMatchA<BOOL,
EvalSimple
oldMemBits: ARRAY quadIndex 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]]];
};
FOR i:quadIndex
IN quadIndex
DO
oldMemBits[i] ← quadData[i].Data[TRUE];
ENDLOOP;
TRUSTED {
cp: BitDWord ← CSTD[DESCRIPTOR[CAMPage], 24, 0, 24, BitDWordZero, 24, 0, 24];
ncp: BitDWord ← CSTD[DESCRIPTOR[nCAMPage], 24, 0, 24, BitDWordZero, 24, 0, 24];
cb: BitWord ← CSTW[DESCRIPTOR[CAMBlock], 4, 0, 4, 0, 4, 0, 4];
ncb: BitWord ← CSTW[DESCRIPTOR[nCAMBlock], 4, 0, 4, 0, 4, 0, 4];
IF SenseVMatchA
THEN {
VPSelectAB ← DAND[ncp, VirtualPageAB]=BitDWordZero AND DAND[cp, nVirtualPageAB]=BitDWordZero;
VBlSelectAB ← WAND[ncb, BlockAB]=0 AND WAND[cb, nBlockAB]=0;
};
IF SenseRMatchB
THEN {
RPSelectBA ← DAND[ncp, RealPageAB]=BitDWordZero AND DAND[cp, nRealPageAB]=BitDWordZero;
RBlSelectBA ← WAND[ncb, BlockAB]=0 AND WAND[cb, nBlockAB]=0;
};
};
VSelMapAB ← VPValidAB AND VPSelectAB;
VSelCellAB ← VSelMapAB AND VBlSelectAB;
RSelMapBA ← RPValidAB AND RPSelectBA;
RSelCellBA ← RSelMapBA AND RBlSelectBA;
IF VSelMapAB
AND PhBb
THEN {
nMapValidB ← FALSE;
IF RPDirtyAB THEN nPageDirtyB ← FALSE;
};
IF VSelCellAB AND PhBb THEN nVirtualBlockMatchB ← FALSE;
IF RSelCellBA AND PhAb THEN nRealBlockMatchA ← FALSE;
DecodeSelectOutBA ← CellAdrBA=thisCellAdr AND CellAdrBA=WNOT[nCellAdrBA, 7];
IF SenseVictimA THEN VictimSelectAB ← DecodeSelectInBA;
IF
NOT PhAb
THEN {
RPAccessA ← FALSE;
BlockAccessA ← FALSE;
VPAccessA ← FALSE;
DataSelectA ← FALSE;
FlagSelectA ← FALSE;
};
IF PhAb
THEN {
IF (SelMapAdrBA AND VSelMapAB) OR (SelRPDecoderBA AND DecodeSelectOutBA) OR (SelRPVictimBA AND VictimSelectAB) THEN RPAccessA ← TRUE;
IF (SelRPDecoderBA AND DecodeSelectOutBA) OR (SelRPVictimBA AND VictimSelectAB) THEN BlockAccessA ← TRUE;
IF (SelOrphanAdrBA AND RSelCellBA) OR (SelVPBA AND DecodeSelectOutBA) THEN VPAccessA ← TRUE;
IF (SelRealDataBA AND RSelCellBA) OR (DecodeSelectOutBA AND SelDecodeBA) OR ForceAllDataSelectsBA THEN DataSelectA ← TRUE;
IF (SelPageFlagsBA AND RSelMapBA) OR DataSelectA THEN FlagSelectA ← TRUE;
};
[RPValidBitA, nRPValidBitA, RPValidAB, nRPValidAB] ← RWB[DataSelectA, RPValidBitA, nRPValidBitA, RPValidAB, nRPValidAB];
[RPDirtyBitA, nRPDirtyBitA, RPDirtyAB, nRPDirtyAB] ← RWB[FlagSelectA, RPDirtyBitA, nRPDirtyBitA, RPDirtyAB, nRPDirtyAB];
[VPValidBitA, nVPValidBitA, VPValidAB, nVPValidAB] ← RWB[FlagSelectA, VPValidBitA, nVPValidBitA, VPValidAB, nVPValidAB];
TRUSTED {
busD: SwitchMWord ← DESCRIPTOR[CAMPage];
nBusD: SwitchMWord ← DESCRIPTOR[nCAMPage];
[VirtualPageAB, nVirtualPageAB] ← RWD[VPAccessA, busD, nBusD, VirtualPageAB, nVirtualPageAB, 24];
};
TRUSTED {
busD: SwitchMWord ← DESCRIPTOR[CAMPage];
nBusD: SwitchMWord ← DESCRIPTOR[nCAMPage];
[RealPageAB, nRealPageAB] ← RWD[RPAccessA, busD, nBusD, RealPageAB, nRealPageAB, 24];
};
TRUSTED {
busD: SwitchMWord ← DESCRIPTOR[CAMBlock];
nBusD: SwitchMWord ← DESCRIPTOR[nCAMBlock];
[BlockAB, nBlockAB] ← RWW[BlockAccessA, busD, nBusD, BlockAB, nBlockAB, 4];
};
FOR i:quadIndex
IN quadIndex
DO
OPEN quadData[i];
IF NOT PhAb THEN MSelA ← FALSE;
IF PhAb AND EBFW[MQSelBA, 4, i] AND DataSelectA THEN MSelA ← TRUE;
IF PhAb AND RSelCellBA AND EBFW[MatchQSelBA, 4, i] AND ValidAB THEN nRQMatchA ← FALSE;
IF MSelA
THEN {
[QMasterA, nQMasterA, Master, nMaster] ← RWB[MSelA, QMasterA, nQMasterA, Master, nMaster];
[QSharedA, nQSharedA, SharedAB, nSharedAB] ← RWB[MSelA, QSharedA, nQSharedA, SharedAB, nSharedAB];
[QValidA, nQValidA, ValidAB, nValidAB] ← RWB[MSelA, QValidA, nQValidA, ValidAB, nValidAB];
TRUSTED {
busD: SwitchMWord ← DESCRIPTOR[MBitsA];
nBusD: SwitchMWord ← DESCRIPTOR[nMBitsA];
dataFD: BitMWord ← DESCRIPTOR[Data[FALSE]];
dataTD: BitMWord ← DESCRIPTOR[Data[TRUE]];
RWM[MSelA, busD, nBusD, dataTD, dataFD, 132];
};
};
IF PhBb AND VSelCellAB AND SharedAB AND EBFW[PQSelAB, 4, i] THEN nQuadSharedB ← FALSE;
IF PhBb AND VictimSelectAB AND Master THEN nQDirtyB ← IBIW[FALSE, nQDirtyB, 4, i];
IF NOT PhBb THEN PSelB ← FALSE;
IF PhBb AND EBFW[PQSelAB, 4, i] AND VSelCellAB AND (nPStoreAB OR FinishSharedStoreAB OR (RPDirtyAB AND nSharedAB)) THEN PSelB ← TRUE;
IF PhBb AND EBFW[PQSelAB, 4, i] AND VSelCellAB AND ValidAB THEN nVQMatchB ← FALSE;
IF PSelB AND PStoreAB THEN {Master ← TRUE; nMaster ← FALSE};
IF PSelB
THEN
TRUSTED {
busD: SwitchMWord ← DESCRIPTOR[PBitsB];
nBusD: SwitchMWord ← DESCRIPTOR[nPBitsB];
dataFD: BitMWord ← DESCRIPTOR[Data[FALSE]];
dataTD: BitMWord ← DESCRIPTOR[Data[TRUE]];
RWM[PSelB, busD, nBusD, dataTD, dataFD, 132];
};
ENDLOOP;
IF
NOT (quadData[0].MSelA
OR quadData[1].MSelA
OR quadData[2].MSelA
OR quadData[3].MSelA)
THEN
TRUSTED {
dataD: BitMWord ← DESCRIPTOR[quadData[0].Data[FALSE]];
mBusD: SwitchMWord ← DESCRIPTOR[MBitsA];
nMBusD: SwitchMWord ← DESCRIPTOR[nMBitsA];
nQMasterA ← SIBISS[FALSE, nQMasterA, [[none, X], [none, X]]];
QMasterA ← SIBISS[FALSE, QMasterA, [[none, X], [none, X]]];
nQSharedA ← SIBISS[FALSE, nQSharedA, [[none, X], [none, X]]];
QSharedA ← SIBISS[FALSE, QSharedA, [[none, X], [none, X]]];
nQValidA ← SIBISS[FALSE, nQValidA, [[none, X], [none, X]]];
QValidA ← SIBISS[FALSE, QValidA, [[none, X], [none, X]]];
SCMTS[dataD, 132, 0, 132, nMBusD, 132, 0, 132, [[none, X], [none, X]]];
SCMTS[dataD, 132, 0, 132, mBusD, 132, 0, 132, [[none, X], [none, X]]];
};
IF
NOT (quadData[0].PSelB
OR quadData[1].PSelB
OR quadData[2].PSelB
OR quadData[3].PSelB)
THEN
TRUSTED {
dataD: BitMWord ← DESCRIPTOR[quadData[0].Data[FALSE]];
pBusD: SwitchMWord ← DESCRIPTOR[PBitsB];
nPBusD: SwitchMWord ← DESCRIPTOR[nPBitsB];
SCMTS[dataD, 132, 0, 132, nPBusD, 132, 0, 132, [[none, X], [none, X]]];
SCMTS[dataD, 132, 0, 132, pBusD, 132, 0, 132, [[none, X], [none, X]]];
};
Dragon.Assert[NOT Dragon.MoreThanOneOf[quadData[0].MSelA, quadData[1].MSelA, quadData[2].MSelA, quadData[3].MSelA]];
Dragon.Assert[NOT Dragon.MoreThanOneOf[quadData[0].PSelB, quadData[1].PSelB, quadData[2].PSelB, quadData[3].PSelB]];
hexVirtualPage ← ELFD[VirtualPageAB, 24, 0, 24];
hexRealPage ← ELFD[RealPageAB, 24, 0, 24];
hexBlock ← ELFW[BlockAB, 6, 0, 6];
TRUSTED {
assembleWord: BitDWord;
diff: BOOL ← FALSE;
FOR i:quadIndex
IN quadIndex
DO
IF oldMemBits[i]#quadData[i].Data[TRUE] THEN {diff ← TRUE; EXIT};
ENDLOOP;
IF diff
OR ForceAllDataSelectsBA
THEN
FOR k:quadIndex
IN quadIndex
DO
FOR j:wordIndex
IN wordIndex
DO
desc: BitMWord ← DESCRIPTOR[quadData[k].Data[TRUE]];
FOR i:[0..32)
IN [0..32)
DO
assembleWord ← IBID[EBFM[desc, 132, (4*i)+j], assembleWord, 32, i];
ENDLOOP;
words[k][j] ← ELFD[assembleWord, 32, 0, 32];
parity[k][j] ← EBFM[desc, 132, 128+j];
ENDLOOP;
ENDLOOP;
}