SpecialTest.Rose
Last Edited by: Spreitzer, January 23, 1985 9:36:04 pm PST
Last Edited by: Gasbarro, August 16, 1984 2:34:08 pm PDT
Directory SwitchTypes;
Library Transistors;
Imports BitSwOps, RoseRun;
CEDAR
Strength: TYPE = SwitchTypes.Strength;
StrengthPair: TYPE = RECORD [u, d: Strength];
certainlyHigh: StrengthPair = [driveWeak, none];
maybeEither: StrengthPair = [driveWeak, drive];
certainlyLow: StrengthPair = [none, drive];
;
CELLTYPE "
STInverter"
PORTS [in<BIT-(Special)-(XPhillic), out>BIT-(Special)-(XPhillic)]
EvalSimple
[out.s[u], out.s[d]] ← SELECT in.val FROM
L => certainlyHigh,
X => maybeEither,
H => certainlyLow,
ENDCASE => 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;
};