Things to add to the checks
-- Registers: enable, reset, complementary output
-- Constant: b>32; b=32, v=-1; v=0 (no Vdd); v=1 (no Gnd)
-- eqConstant: same as constant
-- Comparator
-- Muxes: select -> which input; no select; several selects
TestRegister:
PROC [ct: Core.CellType, n:
NAT ← 2 ]
RETURNS [ok:
BOOLEAN] ~ {
ck, en, input, output, noutput, Vdd, Gnd: NAT;
adInput, adMaster, adSlave, adOutput, adnOutput, adOmaster, adOslave, nInputs, nOutputs: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
state: LogicRegsImpl.RegRef;
adInput ← 3;
adMaster ← adInput+n;
adSlave ← adMaster+n;
nInputs ← adSlave+n;
adOutput ← 1;
adnOutput ← adOutput+n;
adOmaster ← adnOutput+n;
adOslave ← adOmaster+n;
nOutputs ← adOslave+n;
[ck, en, input, output, noutput, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "CK", "en", "Input", "Output", "nOutput", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[ck], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[en], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[input], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
Ports.InitTesterDrive[wire: ct.public[noutput], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
state ← NARROW[Rosemary.GetState[simulation, flatRoot]];
table ← TruthTables.BuildTable[nInputs, nOutputs, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[nInputs, nOutputs, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicRegisterR:
PROC [ct: Core.CellType, n:
NAT ← 2]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
Settle:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
tp[ck].l ← in[0];
tp[en].l ← in[1];
tp[r].l ← in[2];
state.prevCK ← in[3];
FOR i:
NAT
IN [0..n)
DO
tp[input].ls[i] ← in[adInput+i];
state.master[i] ← in[adMaster+i];
state.slave[i] ← in[adSlave+i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[nOutputs]];
out[0] ← state.prevCK;
FOR i:
NAT
IN [0..n)
DO
out[adOutput+i] ← tp[output].ls[i];
out[adnOutput+i] ← tp[noutput].ls[i];
out[adOmaster+i] ← state.master[i];
out[adOslave+i] ← state.slave[i];
ENDLOOP;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
ck, en, r, input, output, noutput, Vdd, Gnd: NAT;
adInput, adMaster, adSlave, adOutput, adnOutput, adOmaster, adOslave, nInputs, nOutputs: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
state: LogicRegsImpl.RegRef;
adInput ← 4;
adMaster ← adInput+n;
adSlave ← adMaster+n;
nInputs ← adSlave+n;
adOutput ← 1;
adnOutput ← adOutput+n;
adOmaster ← adnOutput+n;
adOslave ← adOmaster+n;
nOutputs ← adOslave+n;
[ck, en, r, input, output, noutput, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "CK", "en", "r", "Input", "Output", "nOutput", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[ck], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[en], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[r], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[input], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
Ports.InitTesterDrive[wire: ct.public[noutput], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
state ← NARROW[Rosemary.GetState[simulation, flatRoot]];
table ← TruthTables.BuildTable[nInputs, nOutputs, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[nInputs, nOutputs, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicRegisterSimple:
PROC [ct: Core.CellType, n:
NAT 𡤂]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
Settle:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
tp[ck].l ← in[0];
state.prevCK ← in[1];
FOR i:
NAT
IN [0..n)
DO
tp[input].ls[i] ← in[adInput+i];
state.master[i] ← in[adMaster+i];
state.slave[i] ← in[adSlave+i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[nOutputs]];
out[0] ← state.prevCK;
FOR i:
NAT
IN [0..n)
DO
out[adOutput+i] ← tp[output].ls[i];
out[adnOutput+i] ← tp[noutput].ls[i];
out[adOmaster+i] ← state.master[i];
out[adOslave+i] ← state.slave[i];
ENDLOOP;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
ck, input, output, noutput, Vdd, Gnd: NAT;
adInput, adMaster, adSlave, adOutput, adnOutput, adOmaster, adOslave, nInputs, nOutputs: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
state: LogicRegsImpl.RegRef;
adInput ← 1;
adMaster ← adInput+n;
adSlave ← adMaster+n;
nInputs ← adSlave+n;
adOutput ← 1;
adnOutput ← adOutput+n;
adOmaster ← adnOutput+n;
adOslave ← adOmaster+n;
nOutputs ← adOslave+n;
[ck, input, output, noutput, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "CK", "Input", "Output", "nOutput", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[ck], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[input], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
Ports.InitTesterDrive[wire: ct.public[noutput], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
state ← NARROW[Rosemary.GetState[simulation, flatRoot]];
table ← TruthTables.BuildTable[nInputs, nOutputs, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[nInputs, nOutputs, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicTristateBuffer:
PROC [ct: Core.CellType, n:
NAT 𡤂]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
Settle:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
tp[enable].l ← in[0];
FOR i:
NAT
IN [0..n)
DO
tp[input].ls[i] ← in[1+i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[n]];
FOR i:
NAT
IN [0..n)
DO
out[i] ← tp[output].ls[i];
ENDLOOP;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
input, output, enable, Vdd, Gnd: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
[input, output, enable, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "Input", "Output", "enable", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[input], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[enable], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
table ← TruthTables.BuildTable[n+1, n, Settle, withX];
tableNoX ← TruthTables.BuildTable[n+1, n, Settle, withX];
withX ← FALSE;
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicLatch:
PROC [ct: Core.CellType, n:
NAT ← 2]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
Settle:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
tp[ck].l ← in[0];
FOR i:
NAT
IN [0..n)
DO
tp[input].ls[i] ← in[1+i];
state.master[i] ← in[n+1+i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[n]];
FOR i:
NAT
IN [0..n)
DO
out[i] ← tp[output].ls[i];
ENDLOOP;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
ck, input, output, Vdd, Gnd: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
state: LogicRegsImpl.RegRef;
[ck, input, output, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "CK", "Input", "Output", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[input], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[ck], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
state ← NARROW[Rosemary.GetState[simulation, flatRoot]];
table ← TruthTables.BuildTable[2*n+1, n, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[2*n+1, n, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicAdder:
PROC [ct: Core.CellType, n:
NAT ← 2]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
T:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
tp[carryin].l ← in[0];
FOR i:
NAT
IN [0..n)
DO
tp[a].ls[i] ← in[1+i];
tp[b].ls[i] ← in[n+1+i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[n+1]];
out[0] ← tp[carryout].l;
FOR i:
NAT
IN [0..n)
DO
out[i+1] ← tp[sum].ls[i];
ENDLOOP;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
a, b, sum, carryin, carryout, Vdd, Gnd: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
[a, b, sum, carryin, carryout, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "A", "B", "Sum", "carryIn", "carryOut", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[a], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[b], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[carryin], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[sum], initDrive: none];
Ports.InitTesterDrive[wire: ct.public[carryout], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
table ← TruthTables.BuildTable[2*n+1, n+1, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[2*n+1, n+1, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
LoopTest: RosemaryUser.TestProc = {
Initialize[p, cellType.public];
FromPtoK[p, Eval,000000000H];
FromPtoK[p, Eval,0FFFFFFFFH];
};
RosemaryUser.RegisterTestProc["LoopTest", LoopTest];
};
TestLogicConstant:
PROC [ct: Core.CellType, n:
NAT ← 2]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
Settle:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[n]];
FOR i:
NAT
IN [0..n)
DO
out[i] ← tp[output].ls[i];
ENDLOOP;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
output, Vdd, Gnd: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
[output, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "Output", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
table ← TruthTables.BuildTable[0, n, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[0, n, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicComparator:
PROC [ct: Core.CellType, n:
NAT ← 2]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
Settle:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
FOR i:
NAT
IN [0..n)
DO
tp[a].ls[i] ← in[i];
tp[b].ls[i] ← in[n+i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[1]];
out[0] ← tp[aeqb].l;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
a, b, aeqb, Vdd, Gnd: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
[a, b, aeqb, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "A", "B", "AEqB", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[a], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[b], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[aeqb], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
table ← TruthTables.BuildTable[2*n, 1, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[2*n, 1, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicEqConstant:
PROC [ct: Core.CellType, n:
NAT ← 2]
RETURNS [ok:
BOOLEAN, table: TruthTables.TruthTable, worst:
ARRAY
BOOLEAN
OF
REAL ←
ALL[0.0]] ~ {
Settle:
PUBLIC
PROC [in: TruthLine]
RETURNS [out: TruthLine] ~ {
FOR i:
NAT
IN [0..n)
DO
tp[input].ls[i] ← in[i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[1]];
out[0] ← tp[output].l;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
input, output, Vdd, Gnd: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
[input, output, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "In", "out", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[input], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
table ← TruthTables.BuildTable[n, 1, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[n, 1, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
MsgDone[ct, worst];
};
TestLogicMuxD: PROC [ct: Core.CellType, n, b: NAT ← 2] RETURNS [ok: BOOLEAN, table: TruthTables.TruthTable, worst: ARRAY BOOLEAN OF REAL ← ALL[0.0]] ~ {
Settle: PUBLIC PROC [in: TruthLine] RETURNS [out: TruthLine] ~ {
tp[ck].l ← in[0];
FOR i: NAT IN [0..n) DO
tp[input].ls[i] ← in[1+i];
state.master[i] ← in[n+1+i];
ENDLOOP;
Rosemary.Settle[simulation];
out ← NEW[TruthElmtRec.value[n]];
FOR i: NAT IN [0..n) DO
out[i] ← tp[output].ls[i];
ENDLOOP;
};
tableNoX: TruthTables.TruthTable;
withX: BOOLEAN ← TRUE;
select, input, output, Vdd, Gnd: NAT;
tp: Ports.Port;
simulation: Rosemary.Simulation;
[select, input, output, Vdd, Gnd] ← Ports.PortIndexes[ct.public, "Select", "In", "Output", "Vdd", "Gnd"];
Ports.InitTesterDrive[wire: ct.public[select], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[input], initDrive: force];
Ports.InitTesterDrive[wire: ct.public[output], initDrive: none];
[] ← Rosemary.SetFixedWire[ct.public[Vdd], H];
[] ← Rosemary.SetFixedWire[ct.public[Gnd], L];
tp ← Ports.CreatePort[ct, TRUE];
simulation ← Rosemary.Instantiate[ct, tp, CoreFlat.CreateCutSet[cellTypes: LIST[CoreOps.GetCellTypeName[ct]]]];
Rosemary.Initialize[simulation];
state ← NARROW[Rosemary.GetState[simulation, flatRoot]];
table ← TruthTables.BuildTable[2*n+1, n, Settle, withX];
withX ← FALSE;
tableNoX ← TruthTables.BuildTable[2*n+1, n, Settle, withX];
TruthTables.FillXValues[tableNoX];
ok ← TruthTables.Equal[tableNoX, table];
};