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["AOw", X, Input];
ASh: NAT = Declare["ASh", X, Input];
AVM: NAT = Declare["AVM", X, Input];
FBTIP: NAT = Declare["FBTIP", X, Input];
MyBFault: NAT = Declare["MyBFault", X, Input];
NonFBTIP: NAT = Declare["NonFBTIP", X, Input];
PAccessPermission: NAT = Declare["PAccessPermission", X, Input];
PCmd: NAT = DeclareS["PCmd", NumPCmdBits, Xs, Input];
PCWSEq: NAT = Declare["PCWSEq", X, InputXAllowed];
RamForP: NAT = Declare["RamForP", X, Input];
RCamForP: NAT = Declare["RCamForP", X, Input];
RPValid: NAT = Declare["RPValid", X, Input];
TimeOut: NAT = Declare["TimeOut", X, Input];
PC: NAT = DeclareS["PC", NumPCBits, Xs, Input];
Stack: NAT = DeclareS["Stack", NumStackBits, Xs, InputXAllowed];
Reset: NAT = Declare["Reset", X, Input];
PCtlABusCmd: NAT = DeclareS["PCtlABusCmd", 4, ABusPAdd, Output];
PCtlBCmd: NAT = DeclareS["PCtlBCmd", 4, Xs, Output];
PCtlBusy: NAT = Declare["PCtlBusy", H, Output];
PCtlCSCmd: NAT = DeclareS["PCtlCSCmd", 2, SCmdNoOp, Output];
PCtlDBusCmd: NAT = DeclareS["PCtlDBusCmd", 2, DBusNoOp, Output];
PCtlEnCamSel: NAT = Declare["PCtlEnCamSel", L, Output];
PCtlEnCamSelExt: NAT = Declare["PCtlEnCamSelExt", L, Output];
PCtlFault: NAT = Declare["PCtlFault", L, Output];
PCtlFaultCode: NAT = DeclareS["PCtlFaultCode", 3, 0, Output];
PCtlFlagsForB: NAT = Declare["PCtlFlagsForB", L, Output];
PCtlPartFMch: NAT = Declare["PCtlPartFMch", L, Output];
PCtlFrzVictim: NAT = Declare["PCtlFrzVictim", L, Output];
PCtlLdFIFO: NAT = Declare["PCtlLdFIFO", L, Output];
PCtlLdRBufDataLo: NAT = Declare["PCtlLdRBufDataLo", L, Output];
PCtlLdRBufDataHi: NAT = Declare["PCtlLdRBufDataHi", L, Output];
PCtlLdRBufHeader: NAT = Declare["PCtlLdRBufHeader", L, Output];
PCtlLdSnooper: NAT = Declare["PCtlLdSnooper", L, Output];
PCtlPartVMch: NAT = Declare["PCtlPartVMch", L, Output];
PCtlRdRam: NAT = Declare["PCtlRdRam", L, Output];
PCtlRdRCam: NAT = Declare["PCtlRdRCam", L, Output];
PCtlRdVCam: NAT = Declare["PCtlRdVCam", L, Output];
PCtlReleaseP: NAT = Declare["PCtlReleaseP", L, Output];
PCtlRSCmd: NAT = DeclareS["PCtlRSCmd", 2, SCmdNoOp, Output];
PCtlSelBFC: NAT = Declare["PCtlSelBFC", L, Output];
PCtlSelRplyData: NAT = Declare["PCtlSelRplyData", L, Output];
PCtlSetFBTIP: NAT = Declare["PCtlSetFBTIP", L, Output];
PCtlSetNonFBTIP: NAT = Declare["PCtlSetNonFBTIP", L, Output];
PCtlSetSnooperValid: NAT = Declare["PCtlSetSnooperValid", L, Output];
PCtlShftVictim: NAT = Declare["PCtlShftVictim", L, Output];
PCtlWtMchVCam: NAT = Declare["PCtlWtMchVCam", L, Output];
PCtlWtRam: NAT = Declare["PCtlWtRam", L, Output];
NxtPC: NAT = DeclareS["NxtPC", NumPCBits, Xs, Output];
NxtStack: NAT = DeclareS["NxtStack", NumStackBits, Xs, Output];
Push: NAT = Declare["Push", L, Output];
Vdd: NAT = Declare["Vdd", X, Power];
Gnd: NAT = Declare["Gnd", X, Power];