-- File: [Indigo]<Sakura>Dragon>DragonCacheControlImpl.sak
-- Dragon Cache
-- 18-Feb-82 15:50:59

DIRECTORY
  DragonCacheControl,
  Inline,
  SakuraRT;
  
DragonCacheImpl: MONITOR
  IMPORTS Inline, SakuraRT
  EXPORTS DragonCacheControl = {

-- The functionality of Dragon cache chip is described under the following 
--conventions: there are two main processes, a process to watch the processor bus
--commands (PbusFetch), and a process to watch the memory bus commands
--(BackDoor, backdoor operations).  Furthermore, PbusFetch cooperates with 
--several other processes to allow overlapping of pipline operations: MProc is a 
--process that is invoked from PbusFetch and invokes Mbus operations directly.  
--Operations associated with Pbus commands are all split into two parts so that 
--they can be piplined.  All the front parts of these operations are inside 
--PbusFetch, so they do not constitute independent processes.  The latter parts 
--are all independent processes.  They are FetchTransport, StoreTransport, and 
--DoMapOpTransport.  

-- Communications among processes:
--Communication between PbusFetch and MProc is done through two global
--variables: DoMProc and MProcDone.  The communication between PbusFetch
--and transport processes, FetchTransport, StoreTransport, and
--DoMapOpTransport, is done by global variables, FetchTransportGo, 
--StoreTransportGo, and DoMapOpTransportGo, and ~Reject for the other
--direction.

-- i) Fetch
--Match on Pbus
--IF success THEN Fetch
--ELSE {
--  IF Victim dirty THEN WriteQuad Victim;
--  Partial Match on Pbus
--  IF ~ success THEN ReadMap;
--  ReadQuad};

--ii) Store
--Match on Pbus
--IF success THEN
--  IF ~Shared THEN
--    IF RpDirty THEN Store to Ram
--    ELSE {SetRpDirty; Store to Ram}
--  ELSE 
--    IF RpDirty THEN WriteSingle
--    ELSE {SetRpDirty; WriteSingle}
--ELSE {
--  IF Victim dirty THEN WriteQuad Victim;
--  PartialMatch;
--  IF ~success THEN ReadMap;
--  ReadQuad;
--  GO TO ii) Store}

Cell: TYPE = RECORD [
  vp: LONG CARDINAL,
  rp: LONG CARDINAL,
  bl: [0..37B],
  D: ARRAY [0..3] OF LONG CARDINAL,
  VpValid, RpValid, RpDirty, CEDirty, Shared, TIP: BOOLEAN];
PbusType: TYPE = RECORD [
  body: SELECT kind: {Instruction, Data} FROM
    Instruction => [vp: LONG CARDINAL -- actually 25 bits --,
      bl: [0..37B],
      word: [0..3]],
    Data => [data: LONG CARDINAL]
    ENDCASE];
MbusType: TYPE = RECORD [
  body: SELECT kind: {Instruction, MapCommand, Data} FROM
    Instruction => [command: MbusCommand,
      rp: LONG CARDINAL -- actually 25 bits --,
      bl: [0..37B],
      word: [0..3]],
    MapCommand => [command: MbusCommand,
      mapop: MapOpKind,
      fault: BOOLEAN,
      vp: LONG CARDINAL],
    Data => [data: LONG CARDINAL]
    ENDCASE];
MbusCommand: TYPE = {ReadQuad, WriteQuad, WriteSingle, NotReady, ReadMap, 
  DoMapOp, SetRpDirty, SetRpDirtyDone};
MapOpKind: TYPE = {SetMap, SetMapFlags, GetMapFlags};
MProcType: TYPE = PROC;

-- Constants
DataArraySize: CARDINAL = 64;

-- Global variables
FetchTransportGo, StoreTransportGo, DoMapOpTransportGo, 
  Grant, Holding, MShared, DoMProc, MProcDone, PRq, NewRq, MRq, Orph, 
  MCMD: BOOLEAN;
Instruction, Reqbus: {Fetch, FetchHold, Store, MapOp, Noop};
DataIndex, VictimIndex: CARDINAL;
RqVP, MVP: LONG CARDINAL;
RqBL, PBL, MBL: [0..37B];
RqData: LONG CARDINAL;
PWord, MWord: [0..3];
PResult: LONG CARDINAL;
PRP, MRP: LONG CARDINAL;
Pbus: PbusType;
Mbus: MbusType;
Data: ARRAY [0..DataArraySize) OF Cell;
MOp: MProcType;
MOResult: LONG CARDINAL;
MRdData: LONG CARDINAL;
MWData: LONG CARDINAL;
MInst: MbusCommand;
MapOp: MapOpKind;


PageFault: SIGNAL = CODE;
WriteViolation: SIGNAL = CODE;



Cache: PUBLIC DEVICE = {
IN PDataIn, MDataIn: LONG CARDINAL, CMDIn, RQ, SharedIn: BOOLEAN
OUT Exception, Reject, SharedOut, CMDOut: BOOLEAN, 
    PDataOut, MDataOut: LONG CARDIANL
GUARDIAN {}
CONTROL {


-- PbusFetch process procedures

PbusFetch: PROC = {
  success: BOOLEAN;
DO
--A (Phase A)
  IF RQ AND ~Reject THEN {
    Exception _ FALSE;
    WITH b: Pbus SELECT FROM
      Instruction => {RqVP _ b.vp; RqBL _ b.bl; PWord _ b.word};
      ENDCASE => ERROR;
    Instruction _ Reqbus;
--M (Phase B)
    [success, DataIndex] _ FullMatch[RqVP, RqBL];
    { ENABLE {
        PageFault => {Pbus _ [Data[-1]]; Exception _ TRUE};
        WriteViolation => {Pbus _ [Data[0]]; Exception _ TRUE}};
      SELECT Instruction FROM
        Fetch => CallFetch[];
        FetchHold => CallFetchHold[!
          PageFault => {Pbus _ [Data[-1]]; Holding _ FALSE; Exception _ TRUE}; 
          WriteViolation => {Pbus _ [Data[0]]; Exception _ TRUE}];
        Store => CallStore[];
        MapOp => CallMapOp[];
        Noop => NULL; 
      ENDCASE}
    };
ENDLOOP};

CallFetch: PROC = {
  success: BOOLEAN;
-- Started at Phase B
  IF success THEN { --hit
    Reject _ FALSE;
    FetchTransportGo _ TRUE;
    Holding _ FALSE}
  ELSE {
    Reject _ TRUE;
    Holding _ FALSE;
--R (Phase A)
    Holding _ TRUE;
--T (Phase B)
    PRq _ TRUE;
    WaitForGrant[];
    WriteBackVictimIfDirty[];
    [success, PRP] _ PartialMatch[RqVP];
--Clock (Phase B)
    IF ~success THEN CallMProc[ReadMap];
    CallMProc[ReadQuad];
    PRq _ FALSE;
    Reject _ FALSE;
    [success, DataIndex] _ FullMatch[RqVP, RqBL];
    IF ~success THEN ERROR; -- This is a description error
    FetchTransportGo _ TRUE}
  };

CallFetchHold: PROC = {
-- Started at Phase B
  IF ~Holding THEN {
    Reject _ TRUE;
    PRq _ TRUE;
    WaitForGrant[];
--Clock (Phase B)
    Holding _ TRUE};
  CallFetch[]};

CallStore: PROC = {
  success: BOOLEAN;
  Reject _ TRUE;
-- Clock (A)
  WITH b: Pbus SELECT FROM
    Data => RqData _ b.data;
    ENDCASE => ERROR;
  IF ~success THEN {
    PRq _ TRUE;
    WaitForGrant[];
    WriteBackVictimIfDirty[];
--Clock (Phase B)
    [success, PRP] _ PartialMatch[RqVP];
    IF ~success THEN CallMProc[ReadMap];
--Clock (Phase B)
    CallMProc[ReadQuad]};
--Clock (B)
  [success, DataIndex] _ FullMatch[RqVP, RqBL];
  IF ~Data[DataIndex].Shared THEN {
    IF~Data[DataIndex].RpDirty THEN CallMProc[SetRpDirty];
    Reject _ FALSE;
    StoreTransportGo _ TRUE}
  ELSE {
    IF~Data[DataIndex].RpDirty THEN CallMProc[SetRpDirty];
    Data[DataIndex].D[PWord] _ RqData;
    CallMProc[WriteSingle]};
  PRq _ FALSE;
  }; -- CallStore

CallMapOp: PROC = {
-- Started at Phase B
  Reject _ TRUE;
  PRq _ TRUE;
  WaitForGrant[];
-- Clock (A)
  WITH b: Pbus SELECT FROM
    Data => RqData _ b.data;
    ENDCASE => ERROR;
  CallMProc[DoMapOp];
  PRq _ FALSE}; -- CallMapOp

CallMProc: PROC [procedure: MProcType] = {
-- Starts in Phase B and finishes in Phase B
  MProcDone _ FALSE;
  DoMProc _ TRUE;
  MOp _ procedure;
  DO
--Clock (Phase A)
    IF MProcDone THEN EXIT;
  ENDLOOP}; -- CallMProc

WriteBackVictimIfDirty: PROC = {
-- Starts at Phase A
  MRP _ Data[VictimIndex].rp;
  MBL _ Data[VictimIndex].bl;
  IF Data[VictimIndex].CEDirty THEN {
    CallMProc[WriteQuad];
    Data[VictimIndex].CEDirty _ FALSE};
  }; -- WriteBackVictimIfNotClean

WaitForGrant: PROC = {
  DO
--Clock (Phase A)
    IF Grant THEN EXIT
  ENDLOOP}; -- WaitForGrant



-- FetchTransport process procedures

FetchTransport: PROC = {
-- Starts at Phase A
  DO
--R (Phase A)
    IF FetchTransportGo THEN {
      PResult _ Data[DataIndex].D[PWord];
      FetchTransportGo _ FALSE;
--T (Phase B)
      Pbus _ [Data[PResult]]};
  ENDLOOP};

StoreTransport: PROC = {
-- Starts at Phase A
  DO
  --clock (A)
    IF StoreTransportGo THEN {
      Data[DataIndex].D[PWord] _ RqData;
      StoreTransportGo _ FALSE}
  ENDLOOP}; -- StoreTransport

DoMapOpTransport: PROC = {
  DO
-- clock (B)
  IF DoMapOpTransportGo THEN {
    NewRq _ TRUE;
    MOResult _ MRdData;
    Reject _ FALSE;
--clock (A)
    PResult _ MOResult;
    NewRq _ FALSE;
-- clock (B)
    IF Inline.BITAND[Inline.HighHalf[PResult],40000B]#0 THEN Exception _ TRUE;
    Pbus _ [Data[PResult]]}
  ENDLOOP}; -- DoMapOpTransport



-- MProc process procedures

MProc: PROC = {
DO
--Clock (Phase A)
  MProcDone _ FALSE;
  IF DoMProc THEN {
    DoMProc _ FALSE;
    MOp[]};
ENDLOOP};

WriteQuad: PROC = {
  i: CARDINAL;
  WriteOneWord: PROC [pword: [0..3]] = {
    --Clock (Phase B)
    MWData _ Data[DataIndex].D[pword];
    --Clock (Phase A)
    Mbus _ [Data[MWData]]}; -- WriteOneWord
--Clock (Phase A)
  Mbus _ [Instruction[WriteQuad, MRP, MBL, 0]];
  FOR i IN [0..3] DO WriteOneWord[i] ENDLOOP;
  MProcDone _ TRUE}; -- WriteQuad

ReadMap: PROC = {
  fault: BOOLEAN;
--Clock (Phase A)
  Mbus _ [MapCommand[ReadMap, , , MVP]];
  fault _ WaitMapOpDone[];
  IF fault THEN SIGNAL PageFault;
  MProcDone _ TRUE};

ReadQuad: PROC = {
  ReadOneWord: PROC = {IF ~Orph THEN ReadDataFromBus[@Data[DataIndex].D[PWord]]};
  success: BOOLEAN;
--Clock (Phase A)
  Mbus _ [Instruction[ReadQuad, PRP, PBL, PWord]];
  WITH b: Mbus SELECT FROM
    Instruction => {MRP _ b.rp; MBL _ b.bl; MWord _ b.word};
    ENDCASE => ERROR;
--Clock (Phase B, t2)
  MRq _ TRUE;
--Clock (Phase A, t3)
  [success, DataIndex] _ FullMatch[MRP, MBL];
--Clock (Phase B, t4)
  Orph _ success;
  IF ~success THEN DataIndex _ VictimIndex;
--Clock (Phase A, t5)
  IF ~success THEN {
    Data[DataIndex].rp _ MRP;
    Data[DataIndex].bl _ MBL};
--Clock (Phase B, t6)
  Data[DataIndex].vp _ RqVP;
  Data[DataIndex].Shared _ SharedIn;
  VictimIndex _ (VictimIndex+1) MOD DataArraySize;
--Clock (Phase A, t7)
  MCMD _ CMDIn;
  ReadOneWord[];
  IF MCMD AND MInst=NotReady THEN WaitOneCycle[];
  MProcDone _ TRUE;
--Clock (Phase B, t8)
  ReadOneWord[];
--Clock (Phase A, t9)
  PWord _ (PWord+1) MOD 4;
--Clock (Phase B, t10)
  Data[DataIndex].TIP _ TRUE;
  ReadOneWord[];
  MRq _ FALSE;
  IF ~Holding THEN NewRq _ TRUE;
--Clock (Phase A, t11)
  PWord _ (PWord+1) MOD 4;
--Clock (Phase B, t12)
  ReadOneWord[];
  IF ~Holding THEN NewRq _ FALSE;
--Clock (Phase A, t13)
  PWord _ (PWord+1) MOD 4;
--Clock (Phase B, t14)
  ReadOneWord[];
  Data[DataIndex].TIP _ FALSE};

SetRpDirty: PROC = {
  fault: BOOLEAN;
--Clock (Phase A)
  Mbus _ [Instruction[SetRpDirty, PRP, PBL, PWord]];
  WITH b: Mbus SELECT FROM
    Instruction => {
      MRP _ b.rp;
      MBL _ b.bl;
      MWord _ b.word};
    ENDCASE => ERROR;
--Clock (Phase B)
  fault _ WaitMapOpDone[];
  IF fault THEN SIGNAL WriteViolation;
  MProcDone _ TRUE;
};

WriteSingle: PROC = {
--Clock (Phase A)
  Mbus _ [Instruction[WriteSingle, PRP, PBL, PWord]];
  NewRq _ TRUE;
--Clock (Phase B)
  MWData _ Data[DataIndex].D[PWord];
--Clock (Phase A)
  Mbus _ [Data[MWData]];
  MProcDone _ TRUE;
  NewRq _ FALSE;
};

DoMapOp: PROC = {
  fault: BOOLEAN;
--Clock (Phase A)
  Mbus _ [MapCommand[DoMapOp, MapOp, , MVP]];
  MCMD _ TRUE;
--Clock (Phase B)
  MWData _ RqData;
--Clock (Phase A)
  Mbus _ [Data[MWData]];
  fault _ WaitMapOpDone[];
  IF fault THEN SIGNAL PageFault;
  MProcDone _ TRUE;
  ReadDataFromBus[@MRdData];
  DoMapOpTransportGo _ TRUE}; -- DoMapOp

WaitMapOpDone: PROC RETURNS [fault: BOOLEAN] = {
  DO
--Clock (Phase A)
    MCMD _ CMDIn;
    [MInst, fault] _ DecodeMbusCommand[];
    IF MCMD AND MInst=SetRpDirtyDone THEN EXIT;
  ENDLOOP;
};

DecodeMbusCommand: PROC RETURNS [MInst: MbusCommand, fault: BOOLEAN] = {
  WITH b: Mbus SELECT FROM
    MapCommand => {MInst _ b.command; fault _ b.fault};
    ENDCASE => ERROR};
      
WaitOneCycle: PROC = {
--Clock (Phase B)
--Clock (Phase A)
};



-- Backdoor process procedures

BackDoor: PROC = {
  DO
-- clock (B)
    MCMD _ CMDIn;
    [MInst, ] _ DecodeMbusCommand[];
    IF MCMD THEN
      SELECT MInst FROM
        ReadQuad => BDReadQuad[];
        WriteQuad => BDWriteQuad[];
        WriteSingle => BDWriteSingle[];
        ReadMap => NULL;
        SetRpDirty  => BDSetRpDirty[];
        DoMapOp  => NULL;
      ENDCASE;
  ENDLOOP};

BDReadQuad: PROC = {
  success: BOOLEAN;
  ReadOneWord: PROC = {
  -- clock (B)
    IF success THEN MWData _ Data[DataIndex].D[MWord];
  -- clock (A)
    IF success THEN Mbus _ [Data[MWData]];
    MWord _ (MWord+1) MOD 4;
  };
  [success, DataIndex] _ FullMatch[MRP, MBL];
-- clock (A)
  IF success THEN MShared _ TRUE;
  THROUGH [1..4] DO ReadOneWord[] ENDLOOP;
-- clock (B)
  MShared _ FALSE}; -- BDReadQuad

BDWriteQuad: PROC = {
  success: BOOLEAN;
  WriteOneWord: PROC = {
  -- clock (B)
    IF success THEN Data[DataIndex].D[MWord] _ MRdData;
  -- clock (A)
    MWord _ MWord+1; 
    ReadDataFromBus[@MRdData]};
  [success, DataIndex] _ FullMatch[MRP, MBL];
-- clock (A)
  IF success THEN {
    MShared _ TRUE; MWord _ 0; 
    ReadDataFromBus[@MRdData]};
  THROUGH [1..3] DO WriteOneWord[] ENDLOOP;
-- clock (B)
  IF success THEN Data[DataIndex].D[MWord] _ MRdData;
  IF success THEN MShared _ FALSE}; -- BDWriteQuad

BDWriteSingle: PROC = {
  success: BOOLEAN;
  [success, DataIndex] _ FullMatch[MRP, MBL];
-- clock (A)
  ReadDataFromBus[@MRdData];
-- clock (B)
  IF success THEN Data[DataIndex].D[MWord] _ MRdData};-- BDWriteSingle

BDSetRpDirty: PROC = {
  success: BOOLEAN;
  [success, DataIndex] _ FullMatch[MRP, MBL];
-- clock (A)
-- clock (B)
  IF success THEN Data[DataIndex].RpDirty _ TRUE}; -- BDSetRpDirty
  
ReadDataFromBus: PROC [data: POINTER TO LONG CARDINAL] = {
  WITH b: Mbus SELECT FROM
    Data => data^ _ b.data;
    ENDCASE => ERROR};



-- Data array access procedures

FullMatch: ENTRY PROC [vp: LONG CARDINAL, bl: CARDINAL] RETURNS [BOOLEAN, CARDINAL] = {
  FOR i: CARDINAL IN [0..DataArraySize) DO
    IF Data[i].VpValid AND Data[i].vp=vp AND Data[i].bl=bl THEN
      RETURN [TRUE, i]
    ENDLOOP;
  RETURN[FALSE, 0]};
  
PartialMatch: ENTRY PROC [vp: LONG CARDINAL] RETURNS [BOOLEAN, CARDINAL] = {
  FOR i: CARDINAL IN [0..DataArraySize) DO
    IF Data[i].VpValid AND Data[i].vp=vp THEN
      RETURN [TRUE, i]
    ENDLOOP;
  RETURN[FALSE, 0]};

  
PAR {
    PbusFetch[]
      //
    FetchTransport[]
      //
    StoreTransport[]
      //
    DoMapOpTransport[]
      //
    MProc[]
      //
    BackDoor[]}
  }
};
  
  
  
}.