//====================================================================
//
// 5 stage pipeline: IF, ID, EX, MEM, WB
// Instructions: register-register ALU instructions with 2 register ids
//				 register-immediate ALU instructions with 2 register ids
//				 store instructions
//				 load instructions
//
// Author: Aaron Kobayashi (baudburn at instructor dot net) 
//
// Date:  10/5/02
//
//====================================================================


  (bit
    phi1
    phi2
    phi3
    phi4
    Flush
    Flush_bar

//Regwrite bits
    RegWrite
    IF_RegWrite 
    IF_ID_RegWrite 
    ID_EX_RegWrite
    EX_MEM_RegWrite
    MEM_WB_RegWrite

    write_PC
    write_RegFile_In

    RegsEql_MEMD1
    RegsEql_MEMD2
	RegsEql_WBD1
	RegsEql_WBD2
    fwd_MEMD1
    fwd_MEMD2
  	fwd_WBD1
  	fwd_WBD2
	FwdSelector_D1
	FwdSelector_D2

//Register-Immediate Bits
	use_Imm
	IF_ID_use_Imm
	ID_EX_use_Imm

//Store Instruction Bits
	MemWrite
	IF_MemWrite
	IF_ID_MemWrite
	ID_EX_MemWrite
	EX_MEM_MemWrite
	
	write_DMem_In

//Load Instruction Bits
	MemToReg
	IF_ID_MemToReg
	ID_EX_MemToReg
	EX_MEM_MemToReg
	MEM_WB_MemToReg

	ID_StallReg
	ID_StallReg1
	ID_StallReg2
	ID_WriteResult
	EX_WriteResult
	ID_StallTmp
	ID_Stall
	ID_Stall_bar

    IF_Flush_bar
	
	stall_PC
	IF_ID_phi4
	
	//For Bubbles
	ID_MemWrite
	ID_RegWrite

  )


  (term 
    PC
    sequentialPC

    SrcReg1
    SrcReg2
    DestReg
    Op
    
    Data1
    Data2

	//Inst. Fetch / Decode
    IF_ID_SrcReg1
    IF_ID_SrcReg2
    IF_ID_DestReg
    IF_ID_Op

	//Decode / Execute
    ID_EX_SrcReg1
    ID_EX_SrcReg2
    ID_EX_DestReg
    ID_EX_Op
    ID_EX_Data1
    ID_EX_Data2


	//For forwarding
	FwMux_D1
	FwMux_D2
    EX_Data1
    EX_Data2
    
    Result
    
    EX_MEM_Result
    EX_MEM_DestReg

	MEM_WB_Result
    MEM_WB_DestReg

	//For Reg-Immediate
	Imm
	IF_ID_Imm
	ID_EX_Imm
	ALU_Data2

	//For Store Instructions
	NextMemState
	PresentMemState
		//We have to add opcode and Data2 forwarding to the MEM stage
	EX_DestAddr
	EX_MEM_DestAddr
	EX_MEM_Op

	//For Load Instructions
	ReadData
	MEM_WB_ReadData
	WriteData
  )

  (input phi1 phi2 phi3 phi4 Flush)

  

  // IF Stage Logic
  // ============================================

  //--- Define the PC as a nontransparent latch
  Flush_bar = (not Flush)
 
  //Logic to stall the PC if we are inserting bubbles into the pipeline
  stall_PC  = (and Flush_bar ID_Stall_bar)
  write_PC  = (and phi4 stall_PC)

  (latch PC
    PC            // memory definition name
    (inport 
      write_PC
      (sequentialPC)
    )
    (outport
      phi1
      (PC)
    )
  )


  sequentialPC = (PCAdder PC)
 

  //--- Define the instruction memory
  (memory IMem
    IMem           // memory definition name
    (outport
      phi2 
      PC
      (SrcReg1 SrcReg2 DestReg Op RegWrite Imm use_Imm MemWrite MemToReg)
    )
  )
  
  // Handle flush of pipeline for RegWrites
  IF_RegWrite = (and RegWrite Flush_bar)

  // Handle flush of pipeline for MemWrites
  IF_MemWrite = (and MemWrite Flush_bar)

  // ID Stage Logic
  // ============================================

	//  Since we are stalling at the IF_ID latch, we need to only latch
	//  new data if we are ok to do so
	IF_ID_phi4 = (and phi4 ID_Stall_bar)

	//--- Define the IF/ID latch
  	(latch IF_ID
    IF_ID         // memory definition name
    (inport
      IF_ID_phi4
      (SrcReg1 SrcReg2 DestReg Op IF_RegWrite Imm use_Imm IF_MemWrite
	   MemToReg
      )
    )
    (outport
      phi1
      (IF_ID_SrcReg1 IF_ID_SrcReg2 IF_ID_DestReg IF_ID_Op IF_ID_RegWrite
	  	IF_ID_Imm IF_ID_use_Imm IF_ID_MemWrite IF_ID_MemToReg
      )
    )
	)
  
  
  //--- Define the register file
  write_RegFile_In = (and phi2 MEM_WB_RegWrite)

  (memory RegFile
    RegFile       // memory definition name
    (inport
      write_RegFile_In
      MEM_WB_DestReg
      (WriteData)
    )
    (outport
      phi3
      IF_ID_SrcReg1
      (Data1)
	)
	(outport
	  phi3
      IF_ID_SrcReg2
      (Data2)
    )
  )


//Load-Interlock Logic - Based on information obtained on page A-34 of
//H+P

  //Check if load destination register is one of the source registers
  //in ID
  ID_StallReg1 = (= IF_ID_SrcReg1 ID_EX_DestReg)
  ID_StallReg2 = (= IF_ID_SrcReg2 ID_EX_DestReg)

  //If it is in either case, we might have to stall
  ID_StallReg = (or ID_StallReg1 ID_StallReg2)

  //Check if we will be saving the result, we will need to stall
  ID_WriteResult = (or IF_ID_RegWrite IF_ID_MemWrite)

  //Check if the result in the EX stage will be saved to both memory and
  //to a register file.  If it will not be saved to a register, there is
  //no reason to stall the pipeline
  EX_WriteResult = (and ID_EX_RegWrite ID_EX_MemToReg)

  //If we will be saving the result of the op in the ID stage and the op
  //in the EX stage will be written to memory, we will stall
  ID_StallTmp = (and ID_StallReg ID_WriteResult)
  ID_Stall = (and ID_StallTmp EX_WriteResult)
  ID_Stall_bar = (not ID_Stall)
  
  

  //If we have to stall, we need to insert a bubble in the pipeline.
  //This can be done by not writing back an operation to either the
  //registers or the memory
  ID_MemWrite = (and IF_ID_MemWrite ID_Stall_bar)
  ID_RegWrite = (and IF_ID_RegWrite ID_Stall_bar)


  // EX Stage Logic
  // ============================================

  //--- Define the ID/EX latch
  (latch ID_EX
    ID_EX         // memory definition name
    (inport
      phi4
      (IF_ID_SrcReg1 IF_ID_SrcReg2 IF_ID_DestReg IF_ID_Op ID_RegWrite 
	   Data1 Data2 IF_ID_Imm IF_ID_use_Imm ID_MemWrite IF_ID_MemToReg
      )
    )
    (outport
      phi1
      (ID_EX_SrcReg1 ID_EX_SrcReg2 ID_EX_DestReg ID_EX_Op ID_EX_RegWrite 
 	   ID_EX_Data1 ID_EX_Data2 ID_EX_Imm ID_EX_use_Imm ID_EX_MemWrite
 	   ID_EX_MemToReg
      )
    )
  )


//Forwarding Logic for Data1
	//Fowarding Logic from MEM stage
	RegsEql_MEMD1	= (= EX_MEM_DestReg ID_EX_SrcReg1)
	fwd_MEMD1		= (and RegsEql_MEMD1 EX_MEM_RegWrite)
	FwMux_D1		= (mux fwd_MEMD1 EX_MEM_Result WriteData)

 	//Forwarding Logic for WB Stage
	RegsEql_WBD1 	= (= MEM_WB_DestReg ID_EX_SrcReg1)
	fwd_WBD1		= (and RegsEql_WBD1 MEM_WB_RegWrite)
	
	//Select Forwarded data or New Data
	FwdSelector_D1	= (or fwd_MEMD1 fwd_WBD1)
	EX_Data1	= (mux FwdSelector_D1 FwMux_D1 ID_EX_Data1)

//Forwarding Logic for Data2
	//Fowarding Logic from MEM stage
	RegsEql_MEMD2	= (= EX_MEM_DestReg ID_EX_SrcReg2)
	fwd_MEMD2		= (and RegsEql_MEMD2 EX_MEM_RegWrite)
	FwMux_D2		= (mux fwd_MEMD2 EX_MEM_Result WriteData)

 	//Forwarding Logic for WB Stage
	RegsEql_WBD2 	= (= MEM_WB_DestReg ID_EX_SrcReg2)
	fwd_WBD2		= (and RegsEql_WBD2 MEM_WB_RegWrite)
	
	//Select Forwarded data or New Data
	FwdSelector_D2	= (or fwd_MEMD2 fwd_WBD2)
	EX_Data2	= (mux FwdSelector_D2 FwMux_D2 ID_EX_Data2)
	
//Select between Immediate and Register Data
	ALU_Data2 = (mux ID_EX_use_Imm ID_EX_Imm EX_Data2)

//Destination for Store Instructions
	EX_DestAddr = (buf EX_Data2)

//Compute ALU
  Result = (ALU ID_EX_Op EX_Data1 ALU_Data2)
  

  // MEM Stage Logic
  // ============================================
  //--- Define the ID/EX latch
  (latch EX_MEM
    EX_MEM         // memory definition name
    (inport
      phi4
      (Result ID_EX_DestReg ID_EX_RegWrite ID_EX_MemWrite EX_DestAddr 
	   ID_EX_Op ID_EX_MemToReg
      )
    )
    (outport
      phi1
      (EX_MEM_Result EX_MEM_DestReg EX_MEM_RegWrite EX_MEM_MemWrite
	   EX_MEM_DestAddr EX_MEM_Op EX_MEM_MemToReg
      )
    )
  )

 //--- The data memory, abstracted as a finite state machine
  //    that does not satisfy the forwarding property of the
  //    memory semantics

  write_DMem_In = (and phi4 EX_MEM_MemWrite)

  (latch DMem
    DMem         // memory definition name
    (inport
      write_DMem_In
      (NextMemState)
    )
    (outport
      phi1
      (PresentMemState)
    )
  )

  //--- the next memory state will depend on
  //      -PresentMemState, the present state of the data memory
  //      -Result, the ALU Result (e.g., used as address)
  //      -Data2, the data to be written to that address
  //      -Op, the opcode, as specifying the type of the store
  //       in order to be able to model byte-accesses
  NextMemState = (DMem_Update PresentMemState EX_MEM_Result EX_MEM_DestAddr EX_MEM_Op)


  //--- model a read from address Result of the Data Memory;
  //    the opcode, Op, allows us to model byte-accesses
  ReadData     = (DMem_Read   PresentMemState EX_MEM_Result EX_MEM_Op)
		

  // WB Stage Logic
  // ============================================

  (latch MEM_WB
    MEM_WB         // memory definition name
    (inport
      phi4
      (EX_MEM_DestReg EX_MEM_RegWrite EX_MEM_Result ReadData
	  EX_MEM_MemToReg
      )
    )
    (outport
      phi1
      (MEM_WB_DestReg MEM_WB_RegWrite MEM_WB_Result MEM_WB_ReadData
	  MEM_WB_MemToReg
      )
    )
  )

  
  WriteData = (mux MEM_WB_MemToReg MEM_WB_ReadData MEM_WB_Result)