Vdd, Gnd<BOOL,

LatchBias<BOOL,

PhAb, PhBb<BOOL,

PhAh, PhBh<BOOL,

Resetb<BOOL,

PStore, nPStore>BOOL, PQSel>INT[4],

SenseVMatch>BOOL,

MDoneAB, MHeldAB<BOOL,

MFaultAB<EnumType["Dragon.PBusFaults"],

PAdrHigh, PAdrLowToM>BOOL,

PCmdToMAB>EnumType["Dragon.PBusCommands"],

DoShiftBA, DoExecuteBA<BOOL,

PDataI<INT[32],

DrivePData, DrivePDataI>BOOL,

PCmdI<EnumType["Dragon.PBusCommands"],

PRejectDriveHigh, PRejectDriveLow>BOOL,

PFaultDrive>BOOL,

PFaultI>EnumType["Dragon.PBusFaults"],

PNPErrorDriveLow>BOOL,

ShiftFeedBack, nShiftFeedBack, ShiftEqual, nShiftEqual, ShiftShift, nShiftShift>BOOL,

ShiftDataToPCtl<BOOL,

ShiftDataToPRAMDriver>BOOL,

PDataIToVAReg>BOOL,

ReadVAReg, nReadVAReg>BOOL,

nPBitsPrecharge, MuxRight, MuxLeft, PBitsDrive, nPBitsDrive, PRamRegToPDataI, nPRamRegToPDataI, SensePBits, SensePDataI, ParityIn>BOOL,

ParityOut<BOOL,

ReadPRAMReg, nReadPRAMReg>BOOL

pCmdLatch: PBusCommands,

pShift, npShift: BitWord,

rejectA, rejectB, parityError, parityErrorLatch: BOOL,

isNoOp, suppressVirtualAccess: BOOL,

rejectShift, nrejectShift, parityShift, nparityShift, requestShift, nrequestShift: BOOL,

loadEnable, nloadEnable, loadMustBeOne, nloadMustBeOne, readVA, nreadVA: BOOL,

mask, mustBeOne: BitWord,

pAdrLowShift, npAdrLowShift, pAdrHighShift, npAdrHighShift: BOOL,

requestMatch: BOOL,

ioReference, cacheStoreReference, cacheReference, fetchReference, storeReference, holdReference: BOOL,

shiftExecute, nShiftExecute: BOOL

Assert[NOT MoreThanOneOf[DoShiftBA, DoExecuteBA]];

IF Resetb THEN {

PDataIToVAReg ← PhAh AND NOT rejectB;

IF PDataIToVAReg THEN {

ioReference ← pCmdLatch=IOFetch OR pCmdLatch=IOStore OR pCmdLatch=IOFetchHold OR pCmdLatch=IOStoreHold;

cacheStoreReference ← pCmdLatch=Store OR pCmdLatch=StoreHold;

cacheReference ← pCmdLatch=Fetch OR pCmdLatch=FetchHold OR cacheStoreReference;

fetchReference ← pCmdLatch=Fetch OR pCmdLatch=FetchHold OR pCmdLatch=IOFetch OR pCmdLatch=IOFetchHold;

holdReference ← pCmdLatch=FetchHold OR pCmdLatch=StoreHold OR pCmdLatch=IOFetchHold OR pCmdLatch=IOStoreHold;

storeReference ← cacheStoreReference OR pCmdLatch=IOStore OR pCmdLatch=IOStoreHold;

IF PhBh THEN rejectB ← NOT MDoneAB AND requestMatch AND (ioReference OR (holdReference AND NOT MHeldAB) OR (cacheReference AND (nVirtualMatch OR NOT nMatchTIP)) OR (cacheStoreReference AND (NOT nMatchPageClean OR NOT nMatchCellShared)));

IF PhAb THEN nMatchTIP ← TRUE;

IF PhAh THEN rejectA ← rejectB;

IF PhBh THEN isNoOp ← pCmdLatch=NoOp;

PStore ← cacheStoreReference;

suppressVirtualAccess ← (pCmdLatch=StoreHold AND NOT MHeldAB) OR (NOT cacheReference);

PAdrLow ← NOT suppressVirtualAccess AND PAdrLowToM;

nPAdrLow ← NOT suppressVirtualAccess AND NOT PAdrLowToM;

PCmdToMAB ← IF requestMatch THEN pCmdLatch ELSE NoOp;

PRejectDriveHigh ← PhBb AND requestMatch AND (rejectB OR (MDoneAB AND MFaultAB#None));

PRejectDriveLow ← PhAb;

PFaultDrive ← (PhBb AND requestMatch) OR PhAb;

PFaultI ← IF MDoneAB AND PhBb THEN MFaultAB ELSE None;

ParityIn ← FALSE;

IF PhAh THEN parityError ← ParityOut AND NOT rejectB AND NOT isNoOp;

IF PhBh AND parityError THEN parityErrorLatch ← TRUE;

PNPErrorDriveLow ← parityErrorLatch;

DrivePData ← PhBh AND requestMatch AND fetchReference;

DrivePDataI ← NOT DrivePData;

nPBitsPrecharge ← NOT PhAb;

MuxLeft ← NOT PAdrHigh OR ioReference;

MuxRight ← NOT MuxLeft;

PBitsDrive ← PhBh AND storeReference;

nPBitsDrive ← NOT PBitsDrive;

PRamRegToPDataI ← PhBh AND fetchReference;

nPRamRegToPDataI ← NOT PRamRegToPDataI;

SensePBits ← PRamRegToPDataI;

SensePDataI ← PhBh AND storeReference AND NOT rejectA;

ShiftEqual ← PhBb;

nShiftEqual ← NOT ShiftEqual;

ShiftFeedBack ← PhAb AND NOT (DoShiftBA OR DoExecuteBA);

nShiftFeedBack ← NOT ShiftFeedBack;

ShiftShift ← PhAb AND DoShiftBA;

nShiftShift ← NOT ShiftShift;

shiftExecute ← PhAb AND DoExecuteBA;

nShiftExecute ← NOT shiftExecute;

ShiftToEnable ← (shiftExecute AND loadEnable) OR Resetb;

ShiftToMustBeOne ← (shiftExecute AND loadMustBeOne) OR Resetb;

ReadVAReg ← shiftExecute AND readVA;

nReadVAReg ← NOT ReadVAReg;

ReadPRAMReg ← shiftExecute;

nReadPRAMReg ← nShiftExecute;

IF shiftExecute THEN {

IF ShiftShift THEN {

IF ShiftFeedBack THEN {

IF ShiftEqual THEN {

ShiftDataToPRAMDriver ← pAdrHighShift;