GenInstrDecodePLA5:
PUBLIC GenInstrDecodePLAProc = {
instr: BoolExpr;
temp: BoolExpr;
userMode0: BoolExpr ← BE[m:[userMode0: TRUE], d:[userMode0: TRUE]];
aOpt: BoolExpr ← BE[m:[alpha: 200B], d:[alpha: 200B]];
bOpt: BoolExpr ← BE[m:[alpha: 040B], d:[alpha: 040B]];
cOpt: BoolExpr ← BE[m:[alpha: 100B], d:[alpha: 100B]];
aux: BoolExpr ← BE[m:[alpha: 020B], d:[alpha: 020B]];
src0: BoolExpr ← BE[m:[alpha: 300B], d:[alpha: 0B]];
src1: BoolExpr ← BE[m:[alpha: 300B], d:[alpha: 100B]];
srTop: BoolExpr ← BE[m:[alpha: 200B], d:[alpha: 200B]];
srPop: BoolExpr ← BE[m:[alpha: 300B], d:[alpha: 300B]];
current ← old;
dRR
instr ← And[current, BE[m:[op: InstrTopSig[4]], d:[op: dROR]]];
temp ← And[instr, userMode0];
Set[s: And[temp, Not[ cOpt], aux], m:[beta: 200B], d:[beta: 0], out:[condSel: ModeFault]];
Set[s: And[temp, cOpt ], m:[beta: 200B], d:[beta: 0], out:[condSel: ModeFault]];
Set[s: And[temp, cOpt ], m:[beta: 300B], d:[beta: 200B], out:[condSel: ModeFault]];
AReg
Set[s: And[ Not[aOpt], aux, instr], out:[aReg:[ aBase, beta47]]];
Set[s: And[ Not[aOpt], Not[aux], instr], out:[aReg:[ l, beta47]]];
Set[s: And[aOpt, instr], m:[beta: 010B], d:[beta: 000B], out:[aReg:[ cBase, beta47]]];
Set[s: And[aOpt, instr], m:[beta: 004B], d:[beta: 000B], out:[aReg:[ cBase, beta47]]];
Set[s: And[aOpt, instr], m:[beta: 015B], d:[beta: 014B], out:[aReg:[ s, offset, zero]]];
Set[s: And[aOpt, instr], m:[beta: 015B], d:[beta: 015B], out:[aReg:[ s, offset, minus1]]];
BReg
Set[s: And[ Not[bOpt], aux, instr], out:[bReg:[ aBase, alpha47]]];
Set[s: And[ Not[bOpt], Not[aux], instr], out:[bReg:[ l, alpha47]]];
Set[s: And[bOpt, instr], m:[alpha: 010B], d:[alpha: 000B], out:[bReg:[ cBase, alpha47]]];
Set[s: And[bOpt, instr], m:[alpha: 004B], d:[alpha: 000B], out:[bReg:[ cBase, alpha47]]];
Set[s: And[bOpt, instr], m:[alpha: 015B], d:[alpha: 014B], out:[bReg:[ s, offset, zero]]];
Set[s: And[bOpt, instr], m:[alpha: 015B], d:[alpha: 015B], out:[bReg:[ s, offset, minus1]]];
CReg
Set[s: And[ Not[cOpt], aux, instr], out:[cReg:[ aBase, beta03]]];
Set[s: And[ Not[cOpt], Not[aux], instr], out:[cReg:[ l, beta03]]];
Set[s: And[cOpt, instr], m:[beta: 200B], d:[beta: 000B], out:[cReg:[ cBase, beta03]]];
Set[s: And[cOpt, instr], m:[beta: 100B], d:[beta: 000B], out:[cReg:[ cBase, beta03]]];
Set[s: And[cOpt, instr], m:[beta: 360B], d:[beta: 300B], out:[cReg:[ s, offset, zero]]];
Set[s: And[cOpt, instr], m:[beta: 360B], d:[beta: 320B], out:[cReg:[ s, offset, minus1]]];
Set[s: And[cOpt, instr], m:[beta: 340B], d:[beta: 340B], out:[cReg:[ s, offset, one]]];
Stack
Set[s: And[aOpt, instr], m:[beta: 016B], d:[beta: 016B], out:[popSa: TRUE]];
Set[s: And[bOpt, instr], m:[alpha: 016B], d:[alpha: 016B], out:[popSb: TRUE]];
Set[s: And[cOpt, instr], m:[beta: 340B], d:[beta: 340B], out:[pushSc: TRUE]];
Body of microinstruction with exceptions
Set[s: instr, out:[aluOpIsOp47: TRUE]];
Set[s: instr, m:[op: InstrTopSig[7]], d:[op:dRADD], out:[condSel: OvFl]];
Set[s: instr, m:[op: InstrTopSig[7]], d:[op:dRLADD], out:[condSel: IL]];
Set[s: instr, m:[op: InstrTopSig[8]], d:[op: dRBC], out:[condSel: BC]];
Set[s: instr, m:[op: InstrTopSig[8]], d:[op: dRRX], out:[
dPCmnd: Fetch,
dPCmndIsRd0: TRUE]];
Set[s: instr, m:[op: InstrTopSig[8]], d:[op: dRFU], out:[fCtlIsRtOp0: TRUE]];
Quick Arithmetic Logicals
instr ← And[current, BE[m:[op: InstrTopSig[5]], d:[op: dQOR]]];
Set[s: instr, out: [aluOpIsOp47: TRUE]];
AReg
Set[s: instr, m:[alpha: 300B], d:[alpha: 000B], out:[aReg:[ s, offset, zero]]];
Set[s: instr, m:[alpha: 300B], d:[alpha: 100B], out:[aReg:[ s, offset, zero]]];
Set[s: instr, m:[alpha: 300B], d:[alpha: 200B], out:[aReg:[ cBase, offset, zero]]];
Set[s: instr, m:[alpha: 300B], d:[alpha: 300B], out:[aReg:[ cBase, offset, one]]];
BReg
Set[s: And[ Not[bOpt], aux, instr], out:[bReg:[ aBase, alpha47]]];
Set[s: And[ Not[bOpt], Not[aux], instr], out:[bReg:[ l, alpha47]]];
Set[s: And[bOpt, instr], m:[alpha: 010B], d:[alpha: 000B], out:[bReg:[ cBase, alpha47]]];
Set[s: And[bOpt, instr], m:[alpha: 004B], d:[alpha: 000B], out:[bReg:[ cBase, alpha47]]];
Set[s: And[bOpt, instr], m:[alpha: 015B], d:[alpha: 014B], out:[bReg:[ s, offset, zero]]];
Set[s: And[bOpt, instr], m:[alpha: 015B], d:[alpha: 015B], out:[bReg:[ s, offset, minus1]]];
Set[s: And[bOpt, instr], m:[alpha: 016B], d:[alpha: 016B], out:[popSb: TRUE]];
CReg
Set[s: instr, m:[alpha: 300B], d:[alpha: 000B], out:[cReg:[ s, offset, zero]]];
Set[s: instr, m:[alpha: 100B], d:[alpha: 100B], out:[cReg:[ s, offset, one], pushSc: TRUE]];
Set[s: instr, m:[alpha: 200B], d:[alpha: 200B], out:[cReg:[ s, offset, one], pushSc: TRUE]];
Body of microinstruction with exceptions
Set[s: instr, m:[op: InstrTopSig[7]], d:[op: dQADD], out:[condSel: OvFl]];
Set[s: instr, m:[op: InstrTopSig[7]], d:[op:dQLADD], out:[condSel: IL]];
Set[s: instr, m:[op: InstrTopSig[8]], d:[op: dQBC], out:[condSel: BC]];
Set[s: instr, m:[op: InstrTopSig[8]], d:[op: dQRX], out:[
dPCmnd: Fetch,
dPCmndIsRd0: TRUE]];
Stack Arithmetic Logicals
instr ← And[current, BE[m:[op: InstrTopSig[5]], d:[op: dOR]]];
Set[s: instr, out: [
aluOpIsOp47: TRUE,
aReg: [s, offset, minus1],
bReg: [s, offset, zero],
cReg: [s, offset, minus1],
popSa: TRUE ]];
Set[s: instr, m:[op: InstrTopSig[7]], d:[op: dADD], out:[condSel: OvFl]];
Set[s: instr, m:[op: InstrTopSig[7]], d:[op:dLADD], out:[condSel: IL]];
Set[s: instr, m:[op: InstrTopSig[8]], d:[op: dBC], out:[condSel: BC]];
Set[s: instr, m:[op: InstrTopSig[8]], d:[op: dRX], out:[
dPCmnd: Fetch,
dPCmndIsRd0: TRUE]] };
GenInstrDecodePLAXops: GenInstrDecodePLAProc = {
-- best to be explicit about this
single, double, triple, quintuple: BoolExpr;
current ← old;
single ← BE[m:[op: InstrTopSig[4]], d:[op: x000b]]; -- 16 one byte traps
single ← Or[single, BE[m:[op: InstrTopSig[6]], d:[op: VAL[34B]]]]; -- 4 one byte traps
single ← Or[single, BE[m:[op: InstrTopSig[8]], d:[op: x112b]]]; -- 1 one byte trap
single ← Or[single, BE[m:[op: InstrTopSig[6]], d:[op: x120b]]]; -- 4 one byte traps
single ← Or[single, BE[m:[op: InstrTopSig[8]], d:[op: x125b]]]; -- 1 one byte trap
single ← Or[single, BE[m:[op: InstrTopSig[5]], d:[op: VAL[130B]]]]; -- 8 one byte traps
quintuple ← BE[m:[op: InstrTopSig[4]], d:[op: VAL[040B]]]; -- 16 five byte traps
quintuple ← Or[quintuple, BE[m:[op: InstrTopSig[8]], d:[op: x060b]]]; -- 1 five byte trap
quintuple ← Or[quintuple, BE[m:[op: InstrTopSig[8]], d:[op: x063b]]]; -- 1 five byte trap
quintuple ← Or[quintuple, BE[m:[op: InstrTopSig[5]], d:[op: VAL[070B]]]]; -- 8 five byte traps
double ← BE[m:[op: InstrTopSig[8]], d:[op: x215b]]; -- 1 two byte trap
double ← Or[double, BE[m:[op: InstrTopSig[8]], d:[op: x217b]]]; -- 1 two byte trap
double ← Or[double, BE[m:[op: InstrTopSig[8]], d:[op: x223b]]]; -- 1 two byte trap
double ← Or[double, BE[m:[op: InstrTopSig[8]], d:[op: x234b]]]; -- 1 two byte trap
double ← Or[double, BE[m:[op: InstrTopSig[8]], d:[op: x235b]]]; -- 1 two byte trap
double ← Or[double, BE[m:[op: InstrTopSig[8]], d:[op: x236b]]]; -- 1 two byte trap
triple ← BE[m:[op: InstrTopSig[6]], d:[op: x364b]]; -- 4 three byte traps
triple ← Or[triple, BE[m:[op: InstrTopSig[6]], d:[op: x374b]]]; -- 4 three byte traps
Set[s: And[ current, single], out: [
nextMacro: jump,
pcNext: fromPCBus,
pcBusSrc: xopGen,
pcPipeSrc: seqPC,
push0: TRUE ]
];
Set[s: And[ current, double], out: [
nextMacro: jump,
pcNext: fromPCBus,
pcBusSrc: xopGen,
pcPipeSrc: seqPC,
push0: TRUE,
x2ALitSource: alpha,
cReg: [s, offset, one],
pushSc: TRUE ]
];
Set[s: And[ current, triple], out: [
nextMacro: jump,
pcNext: fromPCBus,
pcBusSrc: xopGen,
pcPipeSrc: seqPC,
push0: TRUE,
x2ALitSource: alphaBeta,
cReg: [s, offset, one],
pushSc: TRUE ]
];
Set[s: And[ current, quintuple], out: [
nextMacro: jump,
pcNext: fromPCBus,
pcBusSrc: xopGen,
pcPipeSrc: seqPC,
push0: TRUE,
x2ALitSource: alpBetGamDel,
cReg: [s, offset, one],
pushSc: TRUE ]
];
};
instrDecodePLA: PUBLIC PLAOps.PLA;