<> <> <> Directory SwitchTypes; Library Transistors; Imports BitSwOps, RoseRun; <> <> <> <> <> <> <<;>> CELLTYPE "STInverter" PORTS [inBIT-(Special)-(XPhillic)] EvalSimple <<[out.s[u], out.s[d]] _ SELECT in.val FROM>> < certainlyHigh,>> < maybeEither,>> < certainlyLow,>> < ERROR;>> out _ BitSwOps.IBISS[in.val#H, out, u, [none, driveWeak]]; out _ BitSwOps.IBISS[in.val#L, out, d, [none, drive]]; ENDCELLTYPE; CELLTYPE "SpecialTest" PORTS [in1, in2, connect< BIT-(XPhillic), o1, o2> BIT-(XPhillic)] Expand I1: STInverter[in: in1, out: o1]; I2: STInverter[in: in2, out: o2]; P: nE[gate: connect, ch1: o1, ch2: o2] Test T BlackBox o1 _ o2 _ [s: ALL[none], val: X]; FOR in1L: Level IN Level DO in1 _ SVFromLevel[in1L]; FOR in2L: Level IN Level DO in2 _ SVFromLevel[in2L]; FOR cL: Level IN Level DO right1, right2: Signal; connect _ SVFromLevel[cL]; [] _ RoseRun.Eval[handle]; IF in1.val # in1L THEN ERROR; IF in2.val # in2L THEN ERROR; IF connect.val # cL THEN ERROR; right1 _ Not[in1L]; right2 _ Not[in2L]; right1 _ Mux[right1, Limit[cL, right2]]; right2 _ Mux[right2, Limit[cL, right1]]; IF o1.val # LevelFromSignal[right1] THEN ERROR; IF o2.val # LevelFromSignal[right2] THEN ERROR; ENDLOOP; ENDLOOP; ENDLOOP; ENDCELLTYPE; CEDAR Level: TYPE = SwitchTypes.Level; Pos: TYPE = [-3 .. 3]; Signal: TYPE = RECORD [d, u: Pos]; -- u >= d <<-2.5: strongly driven low>> <<-1.5: weakly driven low>> <<-0.5: charged low>> <<+0.5: charged high>> <<+1.5: weakly driven high>> <<+2.5: strongly driven high>> PastStrong: NAT = 3; TweenStrongAndWeak: NAT = 2; TweenWeakAndChage: NAT = 1; LevelFromSignal: PROC [s: Signal] RETURNS [l: Level] = { IF SGN[s.d] * SGN[s.u] < 0 THEN RETURN [X]; l _ SELECT SGN[s.d] + SGN[s.u] FROM < 0 => L, > 0 => H, ENDCASE => ERROR; }; Mux: PROC [a, b: Signal] RETURNS [c: Signal] = { Try: PROC [s1, s2: Signal] RETURNS [worked: BOOL] = { sgn1: INTEGER _ SGN[s1.d] + SGN[s1.u]; worked _ FALSE; IF sgn1 = 0 THEN RETURN [FALSE]; IF SGN[s2.d] * sgn1 >= 0 AND SGN[s2.u] * sgn1 >= 0 THEN { SELECT sgn1 FROM > 0 => c _ [d: MAX[s1.d, s2.d], u: MAX[s1.u, s2.u]]; < 0 => c _ [d: MIN[s1.d, s2.d], u: MIN[s1.u, s2.u]]; ENDCASE => ERROR; RETURN [TRUE]}; SELECT sgn1 FROM > 0 => worked _ s1.d >= -s2.d; < 0 => worked _ s1.u <= -s2.u; ENDCASE => ERROR; IF worked THEN c _ s1}; IF Try[a, b] THEN RETURN; IF Try[b, a] THEN RETURN; c _ [d: MIN[a.d, b.d], u: MAX[a.u, b.u]]; }; MaxPos: PROC [s: Signal] RETURNS [mp: NAT] = {mp _ MAX[ABS[s.d], ABS[s.u]]}; Limit: PROC [l: Level, s: Signal] RETURNS [t: Signal] = { t _ SELECT l FROM L => [0, 0], H => s, X => [d: MIN[s.d, 0], u: MAX[s.u, 0]], ENDCASE => ERROR; }; Not: ARRAY Level OF Signal = [ H: [-PastStrong, -TweenStrongAndWeak], X: [-PastStrong, TweenStrongAndWeak], L: [TweenWeakAndChage, TweenStrongAndWeak]]; SVFromLevel: PROC [l: Level] RETURNS [sv: SwitchTypes.SwitchVal] = { sv _ [ s: [ q: input, u: IF l = L THEN none ELSE input, d: IF l = H THEN none ELSE input], val: l]; }; SGN: PROC [x: INT] RETURNS [s: [-1 .. 1]] = { s _ SELECT x FROM < 0 => -1, = 0 => 0, > 0 => 1, ENDCASE => ERROR; };