//====================================================================
//
// 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
//
// 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
	
  )


  (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
  )

  (input phi1 phi2 phi3 phi4 Flush)

  

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

  //--- Define the PC as a nontransparent latch
  Flush_bar = (not Flush)

  write_PC  = (and phi4 Flush_bar)

  (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)
    )
  )
  
  // 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
  // ============================================

	//--- Define the IF/ID latch
  	(latch IF_ID
    IF_ID         // memory definition name
    (inport
      phi4
      (SrcReg1 SrcReg2 DestReg Op IF_RegWrite Imm use_Imm IF_MemWrite
      )
    )
    (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
      )
    )
	)
  
  
  //--- 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
      (MEM_WB_Result)
    )
    (outport
      phi3
      IF_ID_SrcReg1
      (Data1)
	)
	(outport
	  phi3
      IF_ID_SrcReg2
      (Data2)
    )
  )




  // 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 IF_ID_RegWrite 
	  Data1 Data2 IF_ID_Imm IF_ID_use_Imm IF_ID_MemWrite
      )
    )
    (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
      )
    )
  )


//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 MEM_WB_Result)

 	//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 MEM_WB_Result)

 	//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
      )
    )
    (outport
      phi1
      (EX_MEM_Result EX_MEM_DestReg EX_MEM_RegWrite EX_MEM_MemWrite
	   EX_MEM_DestAddr EX_MEM_Op
      )
    )
  )

 //--- 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)


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

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