-- File: [Indigo]<Sakura>Dragon>DragonBackDoorImpl.sak
-- Backdoor process procedures
--

BackDoor: DEVICE = {
  IN
  OUT
  GUARDIAN {}
  CONTROL {
    DO
      WHEN ClockB UP: NULL;
      MCMD ← CMDIn;
      IF MCMD THEN {
        [MInst, ] ← DecodeMbusCommand[];
        SELECT MInst FROM
          ReadQuad => BDReadQuad[];
          WriteQuad => BDWriteQuad[];
          WriteSingle => BDWriteSingle[];
          ReadMap => NULL;
          SetRpDirty  => BDSetRpDirty[];
          DoMapOp  => NULL;
        ENDCASE};
    ENDLOOP}
};

BDReadQuad: PROC = {
  success: BOOLEAN;
  ReadOneWord: PROC = {
    WHEN ClockB UP: IF success THEN MWData ← Data[DataIndex].D[MWord];
    WHEN ClockA UP: {
      IF success THEN MDataOut ← [Data[MWData]];
      MWord ← (MWord+1) MOD 4};
  };
  [success, DataIndex] ← FullMatch[MRP, MBL];
  WHEN ClockA UP: IF success THEN MShared ← TRUE;
  THROUGH [1..4] DO ReadOneWord[] ENDLOOP;
  WHEN ClockB UP: MShared ← FALSE}; -- BDReadQuad

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

BDWriteSingle: PROC = {
  success: BOOLEAN;
  [success, DataIndex] ← FullMatch[MRP, MBL];
  WHEN ClockA UP: ReadDataFromBus[@MRdData]; --  (A)
  WHEN ClockB UP: IF success THEN Data[DataIndex].D[MWord] ← MRdData};-- BDWriteSingle

BDSetRpDirty: PROC = {
  success: BOOLEAN;
  [success, DataIndex] ← FullMatch[MRP, MBL];
  WHEN ClockA UP: NULL; --  (A)
  WHEN ClockB UP: IF success THEN Data[DataIndex].RpDirty ← TRUE}; -- BDSetRpDirty