NumPCmdBits: NAT = 4;
MaxNumSignals: NAT = 100;
Xs: NAT = LAST[NAT];
ToBeDefined: NAT = Xs;
IndexType: TYPE = {Label, ReturnAddress, IOAddr};
Index: ARRAY IndexType OF NAT ← ALL [0];
ChkPermPC: NAT = Next[Label];
CP1PC: NAT = Next[Label];
CP2PC: NAT = Next[Label];
CP3PC: NAT = Next[Label];
HandleMissPC: NAT = Next[Label];
HM1PC: NAT = Next[Label];
HM2PC: NAT = Next[Label];
HM3PPC: NAT = Next[Label];
HM3nPPC: NAT = Next[Label];
HM3nRPC: NAT = Next[Label];
HMnMPC: NAT = Next[Label];
HMnM11PC: NAT = Next[Label];
HMnM12PC: NAT = Next[Label];
HMnM2PC: NAT = Next[Label];
HMnM3PC: NAT = Next[Label];
HMnM4PC: NAT = Next[Label];
HMRCamReadyPC: NAT = Next[Label];
HMReadRamPC: NAT = Next[Label];
HMReturn1PC: NAT = Next[Label];
HMReturn2PC: NAT = Next[Label];
HMRR2PC: NAT = Next[Label];
HMRR3PC: NAT = Next[Label];
HMRR4PC: NAT = Next[Label];
HMRR5PC: NAT = Next[Label];
HMRR6PC: NAT = Next[Label];
HMRRCVct2PC: NAT = Next[Label];
HMRRCVct3PC: NAT = Next[Label];
HMRRCVct4PC: NAT = Next[Label];
HMRRCVM2PC: NAT = Next[Label];
HMRRCVM3PC: NAT = Next[Label];
HMRRCVM4PC: NAT = Next[Label];
IdlePC: NAT = Next[Label];
IOR2PC: NAT = Next[Label];
IOWritePC: NAT = Next[Label];
PCWS3PC: NAT = Next[Label];
PCWS4PC: NAT = Next[Label];
PCWS5PC: NAT = Next[Label];
PCWS6PC: NAT = Next[Label];
PCWS7PC: NAT = Next[Label];
PCWS8PC: NAT = Next[Label];
PCWS9PC: NAT = Next[Label];
PCWS10PC: NAT = Next[Label];
PCWS11PC: NAT = Next[Label];
PCWS12PC: NAT = Next[Label];
PCWS13PC: NAT = Next[Label];
PCWS14PC: NAT = Next[Label];
PCWS14PrimePC: NAT = Next[Label];
PCWS15PC: NAT = Next[Label];
PCWS16PC: NAT = Next[Label];
PCWS17PC: NAT = Next[Label];
PCWSR2PC: NAT = Next[Label];
PCWSRetryPC: NAT = Next[Label];
PSR2PC: NAT = Next[Label];
PSR2PrimePC: NAT = Next[Label];
PSR3PC: NAT = Next[Label];
PSR4PC: NAT = Next[Label];
PSRetryPC: NAT = Next[Label];
PSRetryPrimePC: NAT = Next[Label];
PSReturn1PC: NAT = Next[Label];
PSReturn2PC: NAT = Next[Label];
PSRCamReadyPC: NAT = Next[Label];
PSRRCVM2PC: NAT = Next[Label];
PSRRCVM3PC: NAT = Next[Label];
PSRRCVM4PC: NAT = Next[Label];
PStorePC: NAT = Next[Label];
ResetPC: NAT = Next[Label];
SBTOF2PC: NAT = Next[Label];
SBTOF3PC: NAT = Next[Label];
SIOAF2PC: NAT = Next[Label];
SIOAF3PC: NAT = Next[Label];
SMAF2PC: NAT = Next[Label];
SMAF3PC: NAT = Next[Label];
StoreBTimeOutFaultPC: NAT = Next[Label];
StoreMemAccessFaultPC: NAT = Next[Label];
StoreIOAccessFaultPC: NAT = Next[Label];
MaxPC: NAT = Next[Label];
FromRead: NAT = Next[ReturnAddress];
FromIORead: NAT = FromRead;
FromWrite: NAT = Next[ReturnAddress];
FromIOWrite: NAT = FromWrite;
FromCWS: NAT = Next[ReturnAddress];
MaxStack: NAT = Next[ReturnAddress];
ABusPAdd: NAT = 0;
ABusRqstBuf: NAT = 1;
ABusVCam: NAT = 4;
-- opCode 5 is forbidden by the hardware
ABusCam: NAT = 6;
ABusRCam: NAT = 7;
ABusIOOld: NAT = 8;
ABusIONew: NAT = 9;
ABusIOAId: NAT = 12;
ABusIOFault: NAT = 13;
ABusFault: NAT = 8;
DBusNoOp: NAT = 0;
DBusPWtLatch: NAT = 1;
DBusRRLatch: NAT = 2;
DBusABus: NAT = 3;
SCmdNoOp: NAT = 0;
SCmdLRM: NAT = 1;
SCmdLVM: NAT = 2;
SCmdVictim: NAT = 3;
PCmdNoOp: NAT = 7;
PCmdRead: NAT = 8;
PCmdWrite: NAT = 9;
PCmdCWS: NAT = 10;
PCmdDeMap: NAT = 11;
PCmdIORead: NAT = 12;
PCmdIOWrite: NAT = 13;
PCmdBIOWrite: NAT = 15;
BCmdBIOW: NAT = ORD[DynaBusInterface.Cmd.BIOWRqst]/2;
BCmdCWS: NAT = ORD[DynaBusInterface.Cmd.CWSRqst]/2;
BCmdDeMap: NAT = ORD[DynaBusInterface.Cmd.DeMapRqst]/2;
BCmdFB: NAT = ORD[DynaBusInterface.Cmd.FBRqst]/2;
BCmdIOR: NAT = ORD[DynaBusInterface.Cmd.IORRqst]/2;
BCmdIOW: NAT = ORD[DynaBusInterface.Cmd.IOWRqst]/2;
BCmdMap: NAT = ORD[DynaBusInterface.Cmd.MapRqst]/2;
BCmdRB: NAT = ORD[DynaBusInterface.Cmd.RBRqst]/2;
BCmdWB: NAT = ORD[DynaBusInterface.Cmd.WBRqst]/2;
BCmdWS: NAT = ORD[DynaBusInterface.Cmd.WSRqst]/2;
FaultMemAccess: NAT = 0;
FaultIOAccess: NAT = 1;
FaultBTimeOut: NAT = 2;
NumPCBits: PUBLIC NAT ← 1+SCUtils.Log2[MaxPC-1];
NumStackBits: PUBLIC NAT ← 1+SCUtils.Log2[MaxStack-1];
SignalType: TYPE = {Input, InputXAllowed, Output, Power};
Signals: TYPE = REF SignalsRec;
SignalsRec:
TYPE =
RECORD [
SEQUENCE size:
NAT
OF
RECORD [
name: ROPE ← NIL,
size: NAT ← 0,
st: SignalType,
default: Level ← X,
defaultS: NAT ← Xs,
index: NAT ← Xs
]
];
The signals:
The declaration below simply creates signals, putting signal foo's characteristics in signals[foo]
signals: Signals ← NEW [SignalsRec[MaxNumSignals]];
numSignals: NAT ← 0;
AOw: NAT = Declare[signals, "AOw", X, Input];
ASh: NAT = Declare[signals, "ASh", X, Input];
AVM: NAT = Declare[signals, "AVM", X, Input];
FBTIP: NAT = Declare[signals, "FBTIP", X, Input];
MyBFault: NAT = Declare[signals, "MyBFault", X, Input];
NonFBTIP: NAT = Declare[signals, "NonFBTIP", X, Input];
PAccessPermission: NAT = Declare[signals, "PAccessPermission", X, Input];
PCmd: NAT = DeclareS[signals, "PCmd", NumPCmdBits, Xs, Input];
PCWSEq: NAT = Declare[signals, "PCWSEq", X, InputXAllowed];
RamForP: NAT = Declare[signals, "RamForP", X, Input];
RCamForP: NAT = Declare[signals, "RCamForP", X, Input];
RPValid: NAT = Declare[signals, "RPValid", X, Input];
TimeOut: NAT = Declare[signals, "TimeOut", X, Input];
PC: NAT = DeclareS[signals, "PC", NumPCBits, Xs, Input];
Stack: NAT = DeclareS[signals, "Stack", NumStackBits, Xs, InputXAllowed];
Reset: NAT = Declare[signals, "Reset", X, Input];
PCtlABusCmd: NAT = DeclareS[signals, "PCtlABusCmd", 4, ABusPAdd, Output];
PCtlBCmd: NAT = DeclareS[signals, "PCtlBCmd", 4, Xs, Output];
PCtlBusy: NAT = Declare[signals, "PCtlBusy", H, Output];
PCtlCSCmd: NAT = DeclareS[signals, "PCtlCSCmd", 2, SCmdNoOp, Output];
PCtlDBusCmd: NAT = DeclareS[signals, "PCtlDBusCmd", 2, DBusNoOp, Output];
PCtlEnCamSel: NAT = Declare[signals, "PCtlEnCamSel", L, Output];
PCtlEnCamSelExt: NAT = Declare[signals, "PCtlEnCamSelExt", L, Output];
PCtlFault: NAT = Declare[signals, "PCtlFault", L, Output];
PCtlFaultCode: NAT = DeclareS[signals, "PCtlFaultCode", 3, 0, Output];
PCtlFlagsForB: NAT = Declare[signals, "PCtlFlagsForB", L, Output];
PCtlPartFMch: NAT = Declare[signals, "PCtlPartFMch", L, Output];
PCtlFrzVictim: NAT = Declare[signals, "PCtlFrzVictim", L, Output];
PCtlLdFIFO: NAT = Declare[signals, "PCtlLdFIFO", L, Output];
PCtlLdRBufDataLo: NAT = Declare[signals, "PCtlLdRBufDataLo", L, Output];
PCtlLdRBufDataHi: NAT = Declare[signals, "PCtlLdRBufDataHi", L, Output];
PCtlLdRBufHeader: NAT = Declare[signals, "PCtlLdRBufHeader", L, Output];
PCtlLdSnooper: NAT = Declare[signals, "PCtlLdSnooper", L, Output];
PCtlPartVMch: NAT = Declare[signals, "PCtlPartVMch", L, Output];
PCtlRdRam: NAT = Declare[signals, "PCtlRdRam", L, Output];
PCtlRdRCam: NAT = Declare[signals, "PCtlRdRCam", L, Output];
PCtlRdVCam: NAT = Declare[signals, "PCtlRdVCam", L, Output];
PCtlReleaseP: NAT = Declare[signals, "PCtlReleaseP", L, Output];
PCtlRSCmd: NAT = DeclareS[signals, "PCtlRSCmd", 2, SCmdNoOp, Output];
PCtlSelBFC: NAT = Declare[signals, "PCtlSelBFC", L, Output];
PCtlSelRplyData: NAT = Declare[signals, "PCtlSelRplyData", L, Output];
PCtlSetFBTIP: NAT = Declare[signals, "PCtlSetFBTIP", L, Output];
PCtlSetNonFBTIP: NAT = Declare[signals, "PCtlSetNonFBTIP", L, Output];
PCtlSetSnooperValid: NAT = Declare[signals, "PCtlSetSnooperValid", L, Output];
PCtlShftVictim: NAT = Declare[signals, "PCtlShftVictim", L, Output];
PCtlWtMchVCam: NAT = Declare[signals, "PCtlWtMchVCam", L, Output];
PCtlWtRam: NAT = Declare[signals, "PCtlWtRam", L, Output];
NxtPC: NAT = DeclareS[signals, "NxtPC", NumPCBits, Xs, Output];
NxtStack: NAT = DeclareS[signals, "NxtStack", NumStackBits, Xs, Output];
Push: NAT = Declare[signals, "Push", L, Output];
Vdd: NAT = Declare[signals, "Vdd", X, Power];
Gnd: NAT = Declare[signals, "Gnd", X, Power];