CellType "
Test2BInverter"
Ports [in<BIT-(XPhillic), out=BIT-(XPhillic), gnd, vdd<BIT]
Expand
pd: unE[in, gnd, out];
pu: unD[out, vdd, out]
EndCellType;
CellType "
Test2B"
Ports [in1, in2, sel1, sel2<BIT-(XPhillic), ans>BIT-(XPhillic), gnd, vdd<BIT]
BlackBoxTest
lastAns: Signal ← [FIRST[Pos], 0];
chargeTested ← ALL[FALSE];
gnd ← [s: [input, none, input], val: L];
vdd ← [s: [input, input, none], val: H];
ans ← [s: [none, none, none], val: X];
FOR in1L: Level
IN Level
DO
in1 ← SVFromLevel[in1L];
FOR in2L: Level
IN Level
DO
IF in2L < in1L THEN LOOP;
in2 ← SVFromLevel[in2L];
FOR sel1L: Level
IN Level
DO
sel1 ← SVFromLevel[sel1L];
FOR sel2L: Level
IN Level
DO
rightAns: Signal;
IF in2L = in1L AND sel2L < sel1L THEN LOOP;
sel2 ← SVFromLevel[sel2L];
[] ← RoseRun.Eval[handle: handle];
IF in1.val # in1L THEN ERROR;
IF in2.val # in2L THEN ERROR;
IF sel1.val # sel1L THEN ERROR;
IF sel2.val # sel2L THEN ERROR;
rightAns ← Mux[
Charge[lastAns],
Mux[Limit[sel1L, Not[in1L]], Limit[sel2L, Not[in2L]]]];
IF ans.val # LevelFromSignal[rightAns] THEN ERROR;
IF MaxPos[rightAns] <= TweenWeakAndChage THEN chargeTested[ans.val] ← TRUE;
lastAns ← rightAns;
ENDLOOP;
ENDLOOP;
ENDLOOP;
ENDLOOP;
Expand
out1, out2: BIT-(XPhillic);
inv1: Test2BInverter[in1, out1];
inv2: Test2BInverter[in2, out2];
pass1: nE[sel1, out1, ans];
pass2: nE[sel2, out2, ans]
EndCellType;
CEDAR
Level: TYPE = SwitchTypes.Level;
chargeTested: ARRAY Level OF BOOL;
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]]};
Charge:
PROC [s: Signal]
RETURNS [t: Signal] =
{t ← [d: MAX[-1, MIN[s.d, 0]], u: MIN[1, MAX[s.u, 0]]]};
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;
};