<> <> <> <> <> <<>> <> <<>> < NonFBTIP.>> DIRECTORY Core, CoreClasses, CoreCreate, CoreFlat, DynaBusInterface, IO, Ports, SCUtils, Rosemary, RosemaryUser, SCP <<>> SCP IMPORTS CoreClasses, CoreCreate, CoreFlat, IO, Ports, Rosemary, SCUtils, TerminalIO EXPORTS SCP ~ BEGIN OPEN SCP 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 ] ]; <> <> 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]; <> Create: PUBLIC PROC [] RETURNS [ct: CellType] = { nameList: LIST OF CoreCreate.WR _ NIL; FOR i: NAT IN [0..numSignals) DO IF signals[i].name=NIL THEN LOOP; IF signals[i].size=0 THEN nameList _ CONS[signals[i].name, nameList] ELSE nameList _ CONS[CoreCreate.Seq[signals[i].name, signals[i].size], nameList] ENDLOOP; ct _ CoreClasses.CreateUnspecified[public: CoreCreate.WireList[nameList, p [] _ Rosemary.BindCellType[cellType: ct, roseClassName: p [] _ CoreFlat.CellTypeCutLabels[ct, "Logic"]; FOR i: NAT IN [0..numSignals) DO IF signals[i].name=NIL THEN LOOP; signals[i].index _ Ports.PortIndex[ct.public, signals[i].name]; ENDLOOP; FOR i: NAT IN [0..numSignals) DO SwitchType: TYPE = RECORD [BOOL, SignalType]; switch: SwitchType _ [signals[i].size=0, signals[i].st]; IF signals[i].name=NIL THEN LOOP; SELECT switch FROM [TRUE, Input] => [] _ Ports.InitPorts[ct, l, none, signals[i].name]; [TRUE, InputXAllowed] => [] _ Ports.InitPorts[ct, l, none, signals[i].name]; [TRUE, Output] => [] _ Ports.InitPorts[ct, l, drive, signals[i].name]; [TRUE, Power] => [] _ Ports.InitPorts[ct, b, none, signals[i].name]; [FALSE, Input] => [] _ Ports.InitPorts[ct, ls, none, signals[i].name]; [FALSE, InputXAllowed] => [] _ Ports.InitPorts[ct, ls, none, signals[i].name]; [FALSE, Output] => [] _ Ports.InitPorts[ct, ls, drive, signals[i].name]; ENDCASE => ERROR; ENDLOOP; }; Init: Rosemary.InitProc = { <<--PROC [cellType: Core.CellType, p: Ports.Port] RETURNS [stateAny: REF ANY _ NIL]-->> }; Simple: Rosemary.EvalProc = { <<--PROC [p: Ports.Port, stateAny: REF ANY]-->> XInInputs: PROC [] RETURNS [BOOL _ FALSE] = { PrintName: PROC [name: ROPE] = { TerminalIO.PutF["*** Input %g is an X\n", IO.rope[name]]; }; FOR i: NAT IN [0..numSignals) DO IF signals[i].name=NIL OR signals[i].st#Input THEN LOOP; IF signals[i].size=0 THEN {IF p[signals[i].index].l=X THEN {PrintName[signals[i].name]; RETURN[TRUE]}} ELSE {IF XInLS[p[signals[i].index].ls] THEN {PrintName[signals[i].name]; RETURN[TRUE]}} ENDLOOP; }; OutputsToX: PROC [] = { FOR i: NAT IN [0..numSignals) DO IF signals[i].name=NIL OR signals[i].st#Output THEN LOOP; IF signals[i].size=0 THEN p[signals[i].index].l _ X ELSE Ports.SetLS[p[signals[i].index].ls, X] ENDLOOP; }; OutputsToDefault: PROC [] = { FOR i: NAT IN [0..numSignals) DO IF signals[i].name=NIL OR signals[i].st#Output THEN LOOP; IF signals[i].size=0 THEN p[signals[i].index].l _ signals[i].default ELSE Ports.LCToLS[signals[i].defaultS, p[signals[i].index].ls] ENDLOOP; }; v: PROC [ix: NAT] RETURNS [BOOL] = { RETURN[p[signals[ix].index].l=H] }; vs: PROC [ix: NAT] RETURNS [NAT] = { RETURN[Ports.LSToLC[p[signals[ix].index].ls]] }; s: PROC [ix: NAT, l: Level] = { p[signals[ix].index].l _ l }; ss: PROC [ix: NAT, c: CARD] = { IF c=Xs THEN Ports.SetLS[p[signals[ix].index].ls, X] ELSE Ports.LCToLS[c, p[signals[ix].index].ls]; }; ReadRCam1: PROC [sCmd: NAT] = { s[PCtlRdRCam, H]; s[PCtlEnCamSel, H]; s[PCtlEnCamSelExt, L]; }; ReadRCam2: PROC [sCmd: NAT] = { s[PCtlRdRCam, H]; s[PCtlEnCamSel, H]; s[PCtlEnCamSelExt, L]; ss[PCtlCSCmd, sCmd]; }; ReadRCam34: PROC [sCmd: NAT] = { ss[PCtlCSCmd, sCmd]; }; <> ReadRam1: PROC [sCmd: NAT, drDBus: {DBus, NoDBus} _ DBus] = { ss[PCtlRSCmd, sCmd]; s[PCtlRdRam, H]; }; <> ReadRam2: PROC [sCmd: NAT, drDBus: {DBus, NoDBus} _ DBus] = { <> IF drDBus = DBus THEN ss[PCtlDBusCmd, DBusRRLatch]; }; <> ReadRam3: PROC [sCmd: NAT, drDBus: {DBus, NoDBus} _ DBus] = { IF drDBus = DBus THEN ss[PCtlDBusCmd, DBusRRLatch]; }; WriteRam1: PROC [sCmd: NAT, data: NAT] = { ss[PCtlRSCmd, sCmd]; s[PCtlWtRam, H]; }; WriteRam2: PROC [sCmd: NAT, data: NAT] = { ss[PCtlRSCmd, sCmd]; ss[PCtlDBusCmd, data]; }; WriteRam3: PROC [sCmd: NAT, data: NAT] = { ss[PCtlDBusCmd, data]; }; Jmp: PROC [dest: NAT] = { IF dest=StoreBTimeOutFaultPC OR dest=StoreMemAccessFaultPC OR dest=StoreIOAccessFaultPC THEN { ss[PCtlABusCmd, ABusIOFault]; s[PCtlWtMchVCam, H]; }; IF dest=IdlePC THEN { s[PCtlBusy, L]; s[PCtlLdRBufDataLo, H]; ss[PCtlDBusCmd, DBusPWtLatch]; }; ss[NxtPC, dest]; }; OutputsToDefault[]; <> IF v[Reset] <> THEN {s[Push, H]; ss[NxtStack, FromRead]; Jmp[ResetPC];} ELSE { IF XInInputs[] THEN {OutputsToX[]; RETURN}; SELECT vs[PC] FROM = ResetPC => { IF TRUE THEN { <> Jmp[IdlePC]; }; }; = IdlePC => { SELECT vs[PCmd] FROM <= PCmdNoOp => { <> Jmp[IdlePC]; }; = PCmdRead => { IF v[AVM] THEN { <> Jmp[IdlePC]; }; IF NOT v[AVM] THEN { <> <> s[PCtlPartVMch , H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromRead]; Jmp[HandleMissPC]; }; }; = PCmdWrite => { IF v[AVM] THEN { <> <> Jmp[PStorePC]; }; IF NOT v[AVM] THEN { <> <> s[PCtlPartVMch, H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromWrite]; Jmp[HandleMissPC]; }; }; = PCmdCWS => { IF v[AVM] THEN { <> ss[PCtlABusCmd, ABusIOOld]; s[PCtlWtMchVCam, H]; Jmp[PCWS3PC]; }; IF NOT v[AVM] THEN { <> <> s[PCtlPartVMch , H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromCWS]; Jmp[HandleMissPC]; }; }; = PCmdIORead => { IF v[AVM] THEN { <> Jmp[IdlePC]; }; IF NOT v[AVM] THEN { <> <> s[PCtlPartFMch , H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromIORead]; Jmp[ChkPermPC]; }; }; = PCmdIOWrite => { IF v[AVM] THEN { <> Jmp[IdlePC]; }; IF NOT v[AVM] THEN { <> <> s[PCtlPartFMch , H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromIOWrite]; Jmp[ChkPermPC]; }; }; = PCmdBIOWrite => { IF TRUE THEN { <> <> <> <> s[PCtlLdRBufHeader, H]; s[PCtlSetNonFBTIP, H]; ss[PCtlBCmd, BCmdBIOW]; ss[PCtlABusCmd, ABusPAdd]; Jmp[PSReturn1PC]; }; }; = PCmdDeMap => { IF TRUE THEN { <> <> <> <> s[PCtlLdRBufHeader, H]; s[PCtlSetNonFBTIP, H]; ss[PCtlBCmd, BCmdDeMap]; ss[PCtlABusCmd, ABusPAdd]; Jmp[PSReturn1PC]; }; }; ENDCASE => ERROR; }; = ChkPermPC => { IF TRUE THEN { <> Jmp[CP1PC]; }; }; = CP1PC => { IF TRUE THEN { <> Jmp[CP2PC]; }; }; = CP2PC => { IF TRUE THEN { <> Jmp[CP3PC]; }; }; = CP3PC => { IF v[AVM] THEN { <> <> Jmp[StoreIOAccessFaultPC]; }; IF NOT v[AVM] THEN { <> <> <> <> <> ss[PCtlABusCmd, ABusPAdd]; s[PCtlLdRBufHeader, H]; ss[PCtlDBusCmd, DBusPWtLatch]; s[PCtlLdRBufDataLo, H]; s[PCtlLdRBufDataHi, H]; s[PCtlSetNonFBTIP, H]; Jmp[PSReturn1PC]; SELECT vs[Stack] FROM =FromIORead => { <> ss[PCtlBCmd, BCmdIOR]; }; = FromIOWrite => { <> ss[PCtlBCmd, BCmdIOW]; }; ENDCASE => ERROR; }; }; = IOR2PC => { IF v[NonFBTIP] AND NOT v[TimeOut] THEN { <> Jmp[IOR2PC]; }; IF v[NonFBTIP] AND v[TimeOut] THEN { <> Jmp[StoreBTimeOutFaultPC]; }; IF NOT v[NonFBTIP] AND v[MyBFault] THEN { <> s[PCtlFault, H]; s[PCtlSelBFC, H]; s[PCtlReleaseP, H]; Jmp[IdlePC]; }; IF NOT v[NonFBTIP] AND NOT v[MyBFault] THEN { <> s[PCtlReleaseP, H]; Jmp[IdlePC]; }; }; = PCWSRetryPC => { IF TRUE THEN { <> <> Jmp[PCWSR2PC]; }; }; = PCWSR2PC => { IF TRUE THEN { <> ss[PCtlABusCmd, ABusIOOld]; s[PCtlWtMchVCam, H]; Jmp[PCWS3PC]; }; }; = PCWS3PC => { IF TRUE THEN { <> <> ReadRam1[SCmdLVM]; Jmp[PCWS4PC]; }; }; = PCWS4PC => { IF v[AVM] THEN { <> <> <> ReadRam2[SCmdLVM]; Jmp[PCWS5PC]; }; IF NOT v[AVM] THEN { <> <> ReadRam2[SCmdLVM]; s[PCtlPartVMch, H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromCWS]; Jmp[HandleMissPC]; }; }; = PCWS5PC => { IF v[RamForP] THEN { <> <> <> s[PCtlLdRBufDataHi, H]; ReadRam3[SCmdLVM]; Jmp[PCWS6PC]; }; IF NOT v[RamForP] THEN { <> <> ReadRam1[SCmdLVM]; Jmp[PCWS4PC]; }; }; = PCWS6PC => { IF TRUE THEN { <> Jmp[PCWS7PC]; }; }; = PCWS7PC => { IF v[PCWSEq] THEN { <> ss[PCtlABusCmd, ABusIONew]; s[PCtlWtMchVCam, H]; Jmp[PCWS8PC]; }; IF NOT v[PCWSEq] THEN { <> Jmp[IdlePC]; }; }; = PCWS8PC => { IF TRUE THEN { <> ReadRam1[SCmdLVM]; Jmp[PCWS9PC]; }; }; = PCWS9PC => { IF TRUE THEN { <> ReadRam2[SCmdLVM]; ss[PCtlABusCmd, ABusPAdd]; s[PCtlWtMchVCam, H]; Jmp[PCWS10PC]; }; }; = PCWS10PC => { IF v[RamForP] THEN { <> <> <> ReadRam3[SCmdLVM]; WriteRam1[SCmdLVM, DBusRRLatch]; Jmp[PCWS11PC]; }; IF NOT v[RamForP] THEN { <> <> ss[PCtlABusCmd, ABusIONew]; s[PCtlWtMchVCam, H]; Jmp[PCWS8PC]; }; }; = PCWS11PC => { IF TRUE THEN { <> <> WriteRam2[SCmdLVM, DBusRRLatch]; Jmp[PCWS12PC]; }; }; = PCWS12PC => { IF v[RamForP] THEN { <> <> <> WriteRam3[SCmdLVM, DBusRRLatch]; s[PCtlWtMchVCam, H]; ss[PCtlABusCmd, ABusPAdd]; Jmp[PCWS13PC]; }; IF NOT v[RamForP] THEN { <> <> ss[PCtlABusCmd, ABusIONew]; s[PCtlWtMchVCam, H]; Jmp[PCWS8PC]; }; }; = PCWS13PC => { IF TRUE THEN { <> <> ReadRCam1 [SCmdLVM]; Jmp[PCWS14PC]; }; }; = PCWS14PC => { IF v[ASh] AND v[RCamForP] THEN { <> <> ReadRCam2[SCmdLVM]; Jmp[PCWS15PC]; }; IF v[ASh] AND NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[PCWS14PrimePC]; }; IF NOT v[ASh] THEN { <> s[PCtlReleaseP, H]; Jmp[IdlePC]; }; }; = PCWS14PrimePC => { IF v[RCamForP] THEN { <> ReadRCam2[SCmdLVM]; Jmp[PCWS15PC]; }; IF NOT v[RCamForP] THEN { <> ReadRCam1[SCmdLVM]; Jmp[PCWS14PrimePC]; }; }; = PCWS15PC => { IF v[RCamForP] THEN { <> <> ReadRCam34[SCmdLVM]; Jmp[PCWS16PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[PCWS14PrimePC]; }; }; = PCWS16PC => { IF v[RCamForP] THEN { <> <> <> s[PCtlSetNonFBTIP, H]; ReadRCam34[SCmdLVM]; Jmp[PCWS17PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[PCWS14PrimePC]; }; }; = PCWS17PC => { IF TRUE THEN { <> s[PCtlLdRBufHeader, H]; ss[PCtlBCmd, BCmdCWS]; ss[PCtlABusCmd, ABusCam]; Jmp[PSReturn2PC]; }; }; = PSRetryPC => { IF TRUE THEN { <> <> WriteRam1[SCmdLVM, DBusPWtLatch]; Jmp[PSR2PC]; }; }; = PSR2PrimePC => { IF v[AVM] THEN { <> WriteRam2[SCmdLVM, DBusPWtLatch]; Jmp[PSR3PC]; }; IF NOT v[AVM] THEN { <> <> s[PCtlPartVMch, H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromWrite]; Jmp[HandleMissPC]; }; }; = PSR2PC => { IF TRUE THEN { <> WriteRam2[SCmdLVM, DBusPWtLatch]; Jmp[PSR3PC]; }; }; = PSR3PC => { IF v[RamForP] THEN { <> WriteRam3[SCmdLVM, DBusPWtLatch]; Jmp[PSR4PC]; }; IF NOT v[RamForP] THEN { <> <> WriteRam1[SCmdLVM, DBusPWtLatch]; Jmp[PSR2PrimePC]; }; }; = PSR4PC => { IF v[AVM] THEN { <> <> Jmp[PStorePC]; }; IF NOT v[AVM] THEN { <> <> s[PCtlPartVMch, H]; s[PCtlWtMchVCam, H]; s[Push, H]; ss[NxtStack, FromWrite]; Jmp[HandleMissPC]; }; }; = PStorePC => { IF v[ASh] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[PSRRCVM2PC]; }; IF NOT v[ASh] THEN { <> <> s[PCtlReleaseP, H]; Jmp[IdlePC]; }; }; = PSRRCVM2PC => { IF v[RCamForP] THEN { <> <> ReadRCam2[SCmdLVM]; Jmp[PSRRCVM3PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[PSRRCVM2PC]; }; }; = PSRRCVM3PC => { IF v[RCamForP] THEN { <> <> ReadRCam34[SCmdLVM]; Jmp[PSRRCVM4PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[PSRRCVM2PC]; }; }; = PSRRCVM4PC => { IF v[RCamForP] THEN { <> <> <> s[PCtlSetNonFBTIP, H]; ReadRCam34[SCmdLVM]; Jmp[PSRCamReadyPC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[PSRRCVM2PC]; }; }; = PSRCamReadyPC => { IF TRUE THEN { <> s[PCtlLdRBufHeader, H]; ss[PCtlBCmd, BCmdWS]; ss[PCtlABusCmd, ABusCam]; Jmp[PSReturn2PC]; }; }; = PSReturn1PC => { <> IF TRUE THEN { Jmp[PSReturn2PC]; }; }; = PSReturn2PC => { IF v[NonFBTIP] AND NOT v[TimeOut] THEN { <> s[PCtlSelRplyData, H]; Jmp[PSReturn2PC]; }; IF v[NonFBTIP] AND v[TimeOut] THEN { <> s[PCtlSelRplyData, H]; Jmp[StoreBTimeOutFaultPC]; }; IF NOT v[NonFBTIP] AND v[MyBFault] THEN { <> s[PCtlFault, H]; s[PCtlSelBFC, H]; s[PCtlReleaseP, H]; s[PCtlSelRplyData, H]; Jmp[IdlePC]; }; IF NOT v[NonFBTIP] AND NOT v[MyBFault] THEN { <> s[PCtlReleaseP, H]; s[PCtlSelRplyData, H]; Jmp[IdlePC]; }; }; = HandleMissPC => { IF TRUE THEN { <> <> <> s[PCtlFrzVictim, H]; Jmp[HM1PC]; }; }; = HM1PC => { IF TRUE THEN { <> <> <> <> ReadRCam1[SCmdLVM]; s[PCtlFrzVictim, H]; Jmp[HM2PC]; }; }; = HM2PC => { IF v[RCamForP] THEN { <> <> <> ReadRCam2[SCmdLVM]; Jmp[HM3PPC]; }; IF NOT v[RCamForP] THEN { <> <> <> ReadRCam1[SCmdLVM]; Jmp[HM3nPPC]; }; }; = HM3PPC => { IF v[AVM] AND v[RCamForP] THEN { <> <> <> ReadRCam34[SCmdLVM]; Jmp[HMRRCVM4PC]; }; IF v[AVM] AND NOT v[RCamForP] THEN { <> <> <> ReadRCam1[SCmdLVM]; Jmp[HMRRCVM2PC]; }; IF NOT v[AVM] THEN { <> ss[PCtlABusCmd, ABusIOAId]; s[PCtlWtMchVCam, H]; Jmp[HMnMPC]; }; }; = HMnMPC => { IF TRUE THEN { <> <> <> s[PCtlLdRBufHeader, H]; ss[PCtlBCmd, BCmdMap]; ss[PCtlABusCmd, ABusPAdd]; ReadRam1[SCmdLVM]; Jmp[HMnM11PC]; }; }; = HMnM11PC => { IF TRUE THEN { <> <> ReadRam2[SCmdLVM]; Jmp[HMnM12PC]; }; }; = HMnM12PC => { IF v[RamForP] THEN { <> <> <> s[PCtlSetNonFBTIP, H]; s[PCtlLdRBufDataLo, H]; s[PCtlLdRBufDataHi, H]; ReadRam3[SCmdLVM]; Jmp[HMnM3PC]; }; IF NOT v[RamForP] THEN { <> <> ReadRam1[SCmdLVM]; Jmp[HMnM11PC]; }; }; = HMnM3PC => { <> IF TRUE THEN { Jmp[HMnM4PC]; }; }; = HMnM4PC => { IF v[NonFBTIP] AND NOT v[TimeOut] THEN { <> s[PCtlFlagsForB, H]; Jmp[HMnM4PC]; }; IF v[NonFBTIP] AND v[TimeOut] THEN { <> Jmp[StoreBTimeOutFaultPC]; }; IF NOT v[NonFBTIP] AND v[MyBFault] THEN { <> s[PCtlFault, H]; s[PCtlSelBFC, H]; s[PCtlReleaseP, H]; Jmp[IdlePC]; }; IF NOT v[NonFBTIP] AND NOT v[MyBFault] THEN { <> <> <> s[PCtlLdRBufHeader, H]; ss[PCtlBCmd, BCmdRB]; ss[PCtlABusCmd, ABusCam]; ReadRCam1[SCmdVictim]; Jmp[HMRRCVct2PC]; }; }; = HM3nPPC => { IF v[AVM] AND v[RCamForP] THEN { <> <> <> ReadRCam2[SCmdLVM]; Jmp[HMRRCVM3PC]; }; IF v[AVM] AND NOT v[RCamForP] THEN { <> <> <> ReadRCam1[SCmdLVM]; Jmp[HMRRCVM2PC]; }; IF NOT v[AVM] THEN { <> ss[PCtlABusCmd, ABusIOAId]; s[PCtlWtMchVCam, H]; Jmp[HMnMPC]; }; }; = HMRRCVM2PC => { IF v[RCamForP] THEN { <> <> ReadRCam2[SCmdLVM]; Jmp[HMRRCVM3PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[HMRRCVM2PC]; }; }; = HMRRCVM3PC => { IF v[RCamForP] THEN { <> <> ReadRCam34[SCmdLVM]; Jmp[HMRRCVM4PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[HMRRCVM2PC]; }; }; = HMRRCVM4PC => { IF v[RCamForP] THEN { <> <> ReadRCam34[SCmdLVM]; Jmp[HMRCamReadyPC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdLVM]; Jmp[HMRRCVM2PC]; }; }; = HMRCamReadyPC => { IF v[PAccessPermission] THEN { <> <> s[PCtlLdRBufHeader, H]; ss[PCtlBCmd, BCmdRB]; ss[PCtlABusCmd, ABusCam]; ReadRCam1[SCmdVictim]; Jmp[HMRRCVct2PC]; }; IF NOT v[PAccessPermission] THEN { <> Jmp[StoreMemAccessFaultPC]; }; }; = HMRRCVct2PC => { IF v[RCamForP] THEN { <> ReadRCam2[SCmdVictim]; Jmp[HMRRCVct3PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdVictim]; Jmp[HMRRCVct2PC]; }; }; = HMRRCVct3PC => { IF v[RCamForP] THEN { <> ReadRCam34[SCmdVictim]; Jmp[HMRRCVct4PC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdVictim]; Jmp[HMRRCVct2PC]; }; }; = HMRRCVct4PC => { IF v[RCamForP] THEN { <> ReadRCam34[SCmdVictim]; Jmp[HMReadRamPC]; }; IF NOT v[RCamForP] THEN { <> <> ReadRCam1[SCmdVictim]; Jmp[HMRRCVct2PC]; }; }; = HMReadRamPC => { IF TRUE THEN { <> <> ReadRam1[SCmdVictim, NoDBus]; ss[PCtlABusCmd, ABusRCam]; s[PCtlLdSnooper, H]; s[PCtlSetSnooperValid, H]; Jmp[HMRR2PC]; }; }; = HMRR2PC => { IF TRUE THEN { <> <> ReadRam2[SCmdVictim, NoDBus]; ss[PCtlDBusCmd, DBusABus]; s[PCtlLdRBufDataLo, H]; s[PCtlLdRBufDataHi, H]; Jmp[HMRR3PC]; }; }; = HMRR3PC => { IF v[RamForP] THEN { <> ReadRam3[SCmdVictim, NoDBus]; Jmp[HMRR4PC]; }; IF NOT v[RamForP] THEN { <> ReadRam1[SCmdVictim, NoDBus]; ss[PCtlABusCmd, ABusRCam]; Jmp[HMRR2PC]; }; }; = HMRR4PC => { IF TRUE THEN { <> Jmp[HMRR5PC]; }; }; <> = HMRR5PC => { IF v[AOw] AND v[RPValid] THEN { <> ss[PCtlBCmd, BCmdFB]; ss[PCtlABusCmd, ABusRCam]; s[PCtlSetFBTIP, H]; s[PCtlLdFIFO, H]; Jmp[HMRR6PC]; }; IF NOT v[AOw] THEN { <> s[PCtlSetNonFBTIP, H]; Jmp[HMReturn1PC]; }; IF NOT v[RPValid] THEN { <> <> <> s[PCtlSetNonFBTIP, H]; Jmp[HMReturn1PC]; }; }; = HMRR6PC => { IF TRUE THEN { <> <> s[PCtlSetNonFBTIP, H]; ss[PCtlABusCmd, ABusRqstBuf]; Jmp[HMReturn1PC]; }; }; = HMReturn1PC => { <> IF TRUE THEN { Jmp[HMReturn2PC]; } }; = HMReturn2PC => { IF v[NonFBTIP] AND NOT v[TimeOut] THEN { <> <> ss[PCtlABusCmd, ABusRqstBuf]; s[PCtlSelRplyData, H]; Jmp[HMReturn2PC]; }; IF v[NonFBTIP] AND v[TimeOut] THEN { <> s[PCtlSelRplyData, H]; Jmp[StoreBTimeOutFaultPC]; }; IF NOT v[NonFBTIP] AND v[MyBFault] THEN { <> s[PCtlFault, H]; s[PCtlSelBFC, H]; s[PCtlReleaseP, H]; s[PCtlSelRplyData, H]; Jmp[IdlePC]; }; IF NOT v[NonFBTIP] AND NOT v[MyBFault] THEN { s[PCtlShftVictim, H]; SELECT vs[Stack] FROM =FromRead => { <> s[PCtlReleaseP, H]; s[PCtlSelRplyData, H]; Jmp[IdlePC]; }; = FromWrite => { <> s[PCtlWtMchVCam, H]; Jmp[PSRetryPC]; }; = FromCWS => { <> s[PCtlWtMchVCam, H]; Jmp[PCWSRetryPC]; }; ENDCASE => ERROR; }; }; = StoreMemAccessFaultPC => { IF TRUE THEN { <> WriteRam1[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultMemAccess]; Jmp[SMAF2PC]; }; }; = SMAF2PC => { IF TRUE THEN { <> WriteRam2[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultMemAccess]; Jmp[SMAF3PC]; }; }; = SMAF3PC => { IF v[RamForP] THEN { <> WriteRam3[SCmdLVM, DBusABus]; s[PCtlFault, H]; ss[PCtlFaultCode, FaultMemAccess]; s[PCtlReleaseP, H]; Jmp[IdlePC]; }; IF NOT v[RamForP] THEN { <> ss[PCtlDBusCmd, DBusABus]; WriteRam1[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultMemAccess]; Jmp[SMAF2PC]; }; }; = StoreBTimeOutFaultPC => { IF TRUE THEN { <> WriteRam1[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultBTimeOut]; Jmp[SBTOF2PC]; }; }; = SBTOF2PC => { IF TRUE THEN { <> WriteRam2[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultBTimeOut]; Jmp[SBTOF3PC]; }; }; = SBTOF3PC => { IF v[RamForP] THEN { <> WriteRam3[SCmdLVM, DBusABus]; s[PCtlFault, H]; ss[PCtlFaultCode, FaultBTimeOut]; s[PCtlReleaseP, H]; Jmp[IdlePC]; }; IF NOT v[RamForP] THEN { <> WriteRam1[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultBTimeOut]; Jmp[SBTOF2PC]; }; }; = StoreIOAccessFaultPC => { IF TRUE THEN { <> WriteRam1[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultIOAccess]; Jmp[SIOAF2PC]; }; }; = SIOAF2PC => { IF TRUE THEN { <> WriteRam2[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultIOAccess]; Jmp[SIOAF3PC]; }; }; = SIOAF3PC => { IF v[RamForP] THEN { <> WriteRam3[SCmdLVM, DBusABus]; s[PCtlFault, H]; ss[PCtlFaultCode, FaultIOAccess]; s[PCtlReleaseP, H]; Jmp[IdlePC]; }; IF NOT v[RamForP] THEN { <> ss[PCtlDBusCmd, DBusABus]; WriteRam1[SCmdLVM, DBusABus]; ss[PCtlABusCmd, ABusFault+FaultIOAccess]; Jmp[SIOAF2PC]; }; }; ENDCASE => ERROR; } }; <> Next: PROC [it: IndexType] RETURNS [index: NAT] = { index _ Index[it]; Index[it] _ Index[it]+1; }; Declare: PROC [name: ROPE, default: Level, st: SignalType] RETURNS [ix: NAT] = { signals[numSignals] _ [name: name, st: st, default: default]; ix _ numSignals; numSignals _ numSignals+1; }; DeclareS: PROC [name: ROPE, size: NAT, defaultS: CARD, st: SignalType] RETURNS [ix: NAT] = { signals[numSignals] _ [name: name, size: size, st: st, defaultS: defaultS]; ix _ numSignals; numSignals _ numSignals+1; }; XInLS: PROC [ls: LevelSequence] RETURNS [BOOL _ FALSE] = { FOR i: NAT IN [0..ls.size) DO IF ls[i]=X THEN RETURN [TRUE] ENDLOOP; }; p <> END.