Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
MODEL DLX1C (* A simple microprocessor based on the DLX design *) (* Instruction Types, and fields: RR: Op, Src1, Src2, Dest R[Dest] <-- Op(R[Src1], R[Src2]); PC++ RI: Op, Src1, Imm, Dest R[Dest] <-- Op(R[Src1], Imm); PC++ LD: Op, Src1, Imm, Dest R[Dest] <-- M[Op(R[Src1], Imm)]; PC++ ST: Op, Src1, Imm, Src2 M[Op(R[Src1], Imm)] <-- R[Src2]; PC++ BR: Op, Src1, Src2, Imm if take(Op, R[Src1], R[Src2]) then PC <-- target(PC, Imm) else PC++ *) (* As a design strategy, we try to minimize the amount of state, even if it means performing multiple decodings of a given instruction as it moves down the pipeline *) (* Instruction types *) typedef ICLASS : enum {RR, RI, LD, ST, BR}; (* Symbolic constants that will be used in both implementation and specification modules *) CONST (* Constant denoting RR instruction type. All others are defined relative to it *) I_RR: TERM; (* Initial state *) pc0 : TERM; (* The initial value of the pc *) rf0 : FUNC[1]; (* The initial value of the register file *) mem0 : TERM; (* The initial state of the data memory *) (* Decoding functions *) ifield: FUNC[1]; (* Get instruction type as TERM *) op: FUNC[1]; (* Get instruction operation *) src1: FUNC[1]; (* Get Reg ID for src1 *) src2: FUNC[1]; (* Get Reg ID for src2 *) dest: FUNC[1]; (* Get Reg ID for dest *) imm: FUNC[1]; (* Get immediate data *) (* Computations *) imem: FUNC[1]; (* Fetches instruction given PC *) alu: FUNC[3]; (* ALU function: op, arg1, arg2 *) take: PRED[3]; (* Take branch?: op, arg1, arg2 *) targ: FUNC[2]; (* PC, Imm *) read: FUNC[2]; (* Mem, Addr *) write: FUNC[3]; (* Mem, Addr, Data *) a : TERM; (* Used as an argument to Lambdas *) i : TERM; (* Used as an argument to Lambdas *) (*********** IMPLEMENTATION MODULE *****************) MODULE impl INPUT flush : TRUTH; (* This is an external variable. It is true in a step when the pipeline is to be flushed in that step *) VAR (* ---- State variables ---- *) pPC : TERM; (* Program counter *) fdInstr: TERM; (* Fetch/decode instruction *) fdType : ICLASS; (* Type of instruction in fetch/decode *) fdPC: TERM; (* PC of fetch/decode instruction *) fdValid: TRUTH; (* Is fetch/decode instruction valid? *) (* Decode Stage *) pRF : FUNC[1]; (* Register file - modeled as a memory *) deInstr: TERM; (* Decode/Execute instruction *) deType: ICLASS; (* Type of instruction in decode/execute *) deArg1: TERM; (* Decode/Execute Argument 1 *) deArg2: TERM; (* Decode/Execute Argument 2 *) dePC: TERM; (* Decode/Execute PC *) deValid: TRUTH; (* Is decode/execute instruction valid? *) (* Execute Stage *) emInstr: TERM; (* Execute/Memory Instruction *) emType: ICLASS; (* type of instruction in execute/memory *) emValue: TERM; (* Execute/Memory ALU output *) emArg2: TERM; (* Execute/Memory Arg2 *) emBranch: TRUTH; (* Execute/Memory Take Branch flag *) emTarget: TERM; (* Execute/Memory Branch Target *) emValid: TRUTH; (* Execute/Memory Valid flag *) (* Memory Stage *) dMem: TERM; (* Data memory state *) mwData: TERM; (* Write back data *) mwDest: TERM; (* Write back destination *) mwValid: TRUTH; (* Valid write back? *) (* --- Macro variables --- *) stall : TRUTH; (* stall signal *) squash: TRUTH; (* Squash instructions following branch *) fwd1 : TERM; (* Forwarded arg1 *) fwd2 : TERM; (* Forwarded arg2 *) aluarg2 : TERM; (* Second ALU input *) (* Function for getting instruction type from intruction *) itype: FUNC[1] of ICLASS; (* Local constants -- used for giving arbitrary start state assignments to pipeline stage registers *) CONST fdpc0 : TERM; fdi0 : TERM; fdvd0 : TRUTH; dei0 : TERM; dea10: TERM; dea20: TERM; depc0: TERM; devd0: TRUTH; emi0: TERM; emv0: TERM; ema20: TERM; embr0: TRUTH; emtgt0: TERM; emvd0: TRUTH; mwda0: TERM; mwde0: TERM; mwvd0: TRUTH; (* Macro definitions *) DEFINE (* Stall when executing instruction is load having destination equal to source of instruction in decode *) stall := (deType = LD) & deValid & fdValid & ((dest(deInstr) = src1(fdInstr)) | ((dest(deInstr) = src2(fdInstr)) & (fdType = RR | fdType = ST | fdType = BR))); (* Squash when branch is taken *) squash := emBranch; (* Actual value of Execute argument 1 *) fwd1 := case (* First priority is to forward from memory stage *) emValid & (emType = RR | emType = RI) & dest(emInstr) = src1(deInstr) : emValue; (* Second is to forward from writeback *) mwValid & mwDest = src1(deInstr) : mwData; (* Otherwise, use value from decode *) default: deArg1; esac; (* Forwarded value of Execute Argument 2 *) fwd2 := case (* First priority is to forward from memory stage *) emValid & (emType = RR | emType = RI) & dest(emInstr) = src2(deInstr) : emValue; (* Next is to forward from writeback *) mwValid & mwDest = src2(deInstr) : mwData; (* Otherwise, use value from decode *) default: deArg2; esac; aluarg2 := case (* For RI, ST, or LD Instruction, just take from instruction *) deType = RI | deType = ST | deType = LD: imm(deInstr); default : fwd2; esac; (* Given instruction i, determine its type. Really want an uninterpreted function that returns values of type ICLASS. This is a way to construct it with uninterpreted term function ifield *) itype := Lambda(i) . case ifield(i) = I_RR : RR; ifield(i) = succ(I_RR) : RI; ifield(i) = succ^3(I_RR) : ST; ifield(i) = succ^2(I_RR) : LD; ifield(i) = succ^4(I_RR) : BR; default : RI; esac; (* State assignments *) ASSIGN init[pPC] := pc0; (* initially arbitary *) next[pPC] := case emBranch : emTarget; (* Branch *) stall | flush : pPC; (* Keep the same *) default : succ(pPC); (* Increment *) esac; (* Fetch Stage *) init[fdInstr] := fdi0; (* initially arbitrary *) next[fdInstr] := case stall: fdInstr; (* Stalling *) default: imem(pPC); (* Read from instruction memory *) esac; init[fdType] := itype(fdi0); (* Always type of instruction *) next[fdType] := itype(next[fdInstr]); init[fdPC] := fdpc0; (* initially arbitary *) next[fdPC] := case stall : fdPC; (* Stalling *) default : pPC; esac; init[fdValid] := fdvd0; (* Initially arbitary *) (* Defer flush until after stalling condition cleared *) next[fdValid] := (stall | ~flush) & ~squash; init[pRF] := rf0; (* initially arbitrary *) next[pRF] := Lambda(a) . case mwValid & (a = mwDest) : mwData; (* Write back value *) default : pRF(a); esac; (* Decode stage *) init[deInstr] := dei0; (* Initially arbitrary *) next[deInstr] := fdInstr; (* Get from pipeline *) init[deType] := itype(dei0); next[deType] := fdType; init[deArg1] := dea10; (* Initially arbitary *) next[deArg1] := next[pRF](src1(fdInstr)); (* Read after write *) init[deArg2] := dea20; (* Initially arbitary *) next[deArg2] := next[pRF](src2(fdInstr)); (* Read after write *) init[dePC] := depc0; (* Initially arbitrary *) next[dePC] := fdPC; init[deValid] := devd0; (* Inject bubble here when stalling *) next[deValid] := ~squash & ~stall & fdValid; (* Execute Stage *) init[emInstr] := emi0; next[emInstr] := deInstr; init[emType] := itype(emi0); next[emType] := deType; init[emValue] := emv0; next[emValue] := alu(op(deInstr), fwd1, aluarg2); init[emArg2] := ema20; next[emArg2] := fwd2; init[emBranch] := emvd0 & itype(emi0) = BR & embr0; (* Conditions for taking branch *) next[emBranch] := ~squash & deValid & deType = BR & take(op(deInstr), fwd1, fwd2); init[emTarget] := emtgt0; next[emTarget] := targ(dePC, imm(deInstr)); init[emValid] := emvd0; next[emValid] := ~squash & deValid; (* Memory Stage *) init[dMem] := mem0; (* FSM model of data memory *) next[dMem] := case emType = ST & emValid: write(dMem, emValue, emArg2); (* Store *) default : dMem; esac; init[mwData] := mwda0; (* Writeback data is result of read for LD, and ALU output otherwise *) next[mwData] := case emType = LD : read(dMem, emValue); default : emValue; esac; init[mwDest] := mwde0; next[mwDest] := dest(emInstr); init[mwValid] := mwvd0; (* Conditions for writeback *) next[mwValid] := emValid & (emType = RI | emType = RR | emType = LD); (*********** SPECIFICATION MODULE *****************) MODULE spec INPUT isa : TRUTH; (* isa is 1 if the specification can make a step, 0 otherwise *) project_impl : TRUTH; (* project_impl is 1 if we must project the implementation's state onto the specification's state, 0 otherwise *) VAR (* State variables *) sPC : TERM; (* The program counter *) sRF : FUNC[1]; (* The register file *) sMem : TERM; (* Data memory *) (* Macro Variables *) instr : TERM; (* Instruction *) sType : ICLASS; (* Type of instruction *) arg1 : TERM; (* First operand *) arg2 : TERM; (* Second operand *) aluval : TERM; (* ALU output value *) writeval : TERM; (* Value to write to destination *) takeBranch : TRUTH; (* Take branch? *) target : TERM; (* Branch target *) CONST pc1 : TERM; (* Initial PC *) rf1 : FUNC[1]; (* Initial RF *) mem1 : TERM; (* Initial data memory *) (* Macro definitions *) DEFINE instr := imem(sPC); (* Fetch the instruction *) sType := impl.itype(instr); arg1 := sRF(src1(instr)); arg2 := case sType = RI | sType = ST | sType = LD: imm(instr); default : sRF(src2(instr)); esac; aluval := alu(op(instr),arg1,arg2); writeval := case sType = LD : read(sMem, aluval); default : aluval; esac; takeBranch := sType = BR & take(op(instr), arg1, arg2); target := targ(sPC, imm(instr)); (* State variable assignments *) ASSIGN init[sPC] := pc1; (* initially arbitrary *) next[sPC] := case project_impl : impl.pPC; (* Copy the implementation PC *) isa & takeBranch : target; (* Branch *) isa : succ(sPC); (* Normal *) default: sPC; esac; init[sRF] := rf1; (* initially arbitrary *) next[sRF] := Lambda ( a ) . case project_impl : impl.pRF(a); (* Copy the implementation RF *) isa & a = dest(instr) & (sType = RI | sType = RR | sType = LD) : writeval; default : sRF(a); esac; init[sMem] := mem1; next[sMem] := case project_impl : impl.dMem; (* Copy the implementation memory *) isa & sType = ST : write(sMem, aluval, sRF(src2(instr))); default : sMem; esac; (***** CONTROL Module *****) CONTROL (* external variable declarations *) EXTVAR (* These variables have already appeared as INPUTs. They are all initialized with a default value of 0. *) flush : TRUTH := 0; isa : TRUTH := 0; project_impl : TRUTH := 0; (* Storage variables. These will be used to store intermediate values during the simulation *) STOREVAR I_pc : TERM; (* Impl PC after 1 step *) I_rf : FUNC[1]; (* Impl RF after 1 step *) I_dm : TERM; (* Impl Data mem after 1 step *) S_pc0 : TERM; (* Spec PC after 0 steps *) S_rf0 : FUNC[1]; (* Spec RF after 0 steps *) S_dm0 : TERM; (* Spec Data mem after 0 steps *) S_pc1 : TERM; (* Spec PC after 1 step *) S_rf1 : FUNC[1]; (* Spec RF after 1 step *) S_dm1 : TERM; (* Spec Data mem after 1 step *) CONST a1 : TERM; (* Argument to a Lambda *) (* Statements begin *) EXEC (*----------------------------------------------------------------*) (* First, we simulate counter-clockwise from the left hand bottom to the right hand top of the diagram *) (* One step of the implementation *) simulate(1); (* We need to flush for 5 steps. So set flush to 1 for the next 5 steps *) flush[1] := 1; flush[2] := 1; flush[3] := 1; flush[4] := 1; flush[5] := 1; simulate(5); (* Store the state of the pipeline after flushing *) I_pc := impl.pPC; I_rf := impl.pRF; I_dm := impl.dMem; (*----------------------------------------------------------------*) (* Reset all state variables to the initial state *) initialize; (*----------------------------------------------------------------*) (* Now, we simulate clockwise from the left hand bottom to the right hand top of the diagram *) (* First flush for five steps *) flush[0] := 1; flush[1] := 1; flush[2] := 1; flush[3] := 1; flush[4] := 1; simulate(5); (* Now project the impl. state onto the spec. *) project_impl[5] := 1; simulate(1); (* Store the spec state variable values after 0 steps *) S_pc0 := spec.sPC; S_rf0 := spec.sRF; S_dm0 := spec.sMem; (* Run the spec machine for 1 step *) isa[6] := 1; simulate(1); (* Store the spec state variable values after 1 step *) S_pc1 := spec.sPC; S_rf1 := spec.sRF; S_dm1 := spec.sMem; (******** check for correspondence ********) (* Do the PC, RF, and data memory correspond, for either 0 or 1 steps of the spec.? *) decide(((S_pc1 = I_pc) & (S_rf1(a1) = I_rf(a1)) & (S_dm1 = I_dm)) | ((S_pc0 = I_pc) & (S_rf0(a1) = I_rf(a1)) & (S_dm0 = I_dm)));