InterlockPLA: PLAOps.PLA;
GenInterlockPLA:
PROC = {
read2: BoolExpr ← BE[m:[dPCmndRd2: TRUE], d:[dPCmndRd2: TRUE]];
read3: BoolExpr ← BE[m:[dPCmndRd3: TRUE], d:[dPCmndRd3: TRUE]];
ac2: BoolExpr ← BE[m:[a1IsC2: TRUE], d:[a1IsC2: TRUE]];
bc2: BoolExpr ← BE[m:[b1IsC2: TRUE], d:[b1IsC2: TRUE]];
ac3: BoolExpr ← BE[m:[a1IsC3: TRUE], d:[a1IsC3: TRUE]];
bc3: BoolExpr ← BE[m:[b1IsC3: TRUE], d:[b1IsC3: TRUE]];
kIsRtOp: BoolExpr ← BE[m:[kIsRtOp1: TRUE], d:[kIsRtOp1: TRUE]];
fCtlIsRtOp: BoolExpr ← BE[m:[fCtlIsRtOp1: TRUE], d:[fCtlIsRtOp1: TRUE]];
cField2: BoolExpr ← BE[m:[cIsField2: TRUE], d:[cIsField2: TRUE]];
cField3: BoolExpr ← BE[m:[cIsField3: TRUE], d:[cIsField3: TRUE]];
isBubble2: BoolExpr ← BE[m:[condEffect2: VAL[LAST[IFUPLAMainControl.CondEffect]]],
d:[condEffect2: bubble]];
aluRtFromB: BoolExpr ← Not[ Or[ kIsRtOp, fCtlIsRtOp ]];
interlock2: BoolExpr ← And[ read2, Or[ ac2, bc2, And[ fCtlIsRtOp, cField2 ]]];
interlock3: BoolExpr ← Or[
Not[isBubble2],
And[ read3, Or[ ac3, bc3, And[ fCtlIsRtOp, cField3 ]]]
];
Pipe Interlock
= stage1BHold OR (DPReject AND stage1BHoldIfReject)
Set[s: interlock2, out: [stage1BHold: TRUE ] ];
Set[s: interlock3, out: [stage1BHoldIfReject: TRUE ] ];