IFUTestComplete:
CEDAR
PROGRAM
IMPORTS CoreCreate, CoreFlat, CoreOps, IFUSim, IO, PLASim, Ports, Rope, Rosemary, RosemaryUser, IFUTest, TerminalIO
EXPORTS IFUTest =
BEGIN
ROPE: TYPE = Core.ROPE;
CellType: TYPE = Core.CellType;
Wire: TYPE = Core.Wire;
StateSeq: TYPE = IFUTest.StateSeq;
QPh: TYPE = IFU2.QPh;
QPhRope: ARRAY QPh OF ROPE ← [A: "A", ab: "ab", B: "B", ba: "ba"];
Signal: SIGNAL = CODE;
II: TYPE = IFU2.II;
PortData: TYPE = RECORD [ name: ROPE, width: NAT ← 1, drive: Ports.Drive ← none ];
iITypes:
ARRAY
II
OF PortData ← [
KBus: ["KBus", 32, force],
EUAluOp2AB: ["EUAluOp2AB", 4, expect],
EUCondSel2AB: ["EUCondSel2AB", 4, expect],
EUCondition2B: ["EUCondition2B", 1, force],
EURdFromPBus3AB: ["EURdFromPBus3AB", 1, expect],
EUWriteToPBus3AB: ["EUWriteToPBus3AB", 1, expect],
UserMode2BA: ["UserMode2BA", 1, expect],
DPCmdA: ["DPCmdA", 8, expect],
DPRejectB: ["DPRejectB", 1, force],
DPFaultB: ["DPFaultB", 4, force],
IPData: ["IPData", 32, force],
IPCmdFetchA: ["IPCmdFetchA", 1, expect],
IPRejectB: ["IPRejectB", 1, force],
IPFaultingB: ["IPFaultingB", 1, force],
DShA: ["DShA", 1, force],
DShB: ["DShB", 1, force],
DShRd: ["DShRd", 1, force],
DShWt: ["DShWt", 1, force],
DShIn: ["DShIn", 1, force],
DShOut: ["DShOut", 1, force],
ResetAB: ["ResetAB", 1, force],
RescheduleAB: ["RescheduleAB", 1, force],
PhA: ["PhA", 1, force],
PhB: ["PhB", 1, force],
NotPhA: ["NotPhA", 1, force],
NotPhB: ["NotPhB", 1, force],
Vdd: ["Vdd", 1, force],
Gnd: ["Gnd", 1, force],
PadVdd: ["PadVdd", 1, force],
PadGnd: ["PadGnd", 1, force] ];
Formality:
PUBLIC
PROC = {
states: StateSeq;
simulation: Rosemary.Simulation;
p: Ports.Port;
display: RosemaryUser.RoseDisplay;
formalTest: ROPE ← "FormalTest";
public: Core.Wire ← NIL;
publics: LIST OF CoreCreate.WR ← NIL;
cell: CellType;
F: BOOL ← FALSE;
cuts: CoreFlat.CutSet ← CoreFlat.CreateCutSet[labels: LIST ["SimplePLA", "UpOneLevel"]];
FOR wireId:
II
DECREASING
IN
II
DO
wr: CoreCreate.
WR ← (
SELECT iITypes[wireId].width
FROM
1 => iITypes[wireId].name,
ENDCASE => CoreCreate.Seq[name: iITypes[wireId].name, size: iITypes[wireId].width]);
publics ← CONS[wr, publics];
ENDLOOP;
public ← CoreCreate.WireList[publics];
cell ← IFUSim.FormalIFU[public, TRUE];
FOR wireId:
II
IN
II
DO
[] ← Ports.InitPort[
wire: cell.public[wireId.ORD],
levelType: (
SELECT iITypes[wireId].width
FROM
1 => b,
<=16 => c,
<=32 => lc,
ENDCASE => ERROR) ];
[] ← Ports.InitTesterDrive[
wire: cell.public[wireId.ORD],
initDrive: iITypes[wireId].drive ];
ENDLOOP;
[] ← Rosemary.SetFixedWire[CoreOps.FindWire[public, "Vdd"], H];
[] ← Rosemary.SetFixedWire[CoreOps.FindWire[public, "Gnd"], L];
[] ← Rosemary.SetFixedWire[CoreOps.FindWire[public, "PadVdd"], H];
[] ← Rosemary.SetFixedWire[CoreOps.FindWire[public, "PadGnd"], L];
p ← Ports.CreatePort[cell, TRUE];
simulation ← Rosemary.Instantiate[cell, p, cuts];
display ← RosemaryUser.DisplayViewer
[simulation, cell, formalTest, RosemaryUser.DisplayPortLeafWires[cell]];
RosemaryUser.InitializeDeltas[display];
states ← IFUTest.InitStates[simulation, 8];
p[ II[ KBus ].ORD ].lc ← 0;
p[ II[ EUAluOp2AB ].ORD ].c ← 0;
p[ II[ EUCondSel2AB ].ORD ].c ← 0;
p[ II[ EUCondition2B ].ORD ].b ← F;
p[ II[ EURdFromPBus3AB ].ORD ].b ← F;
p[ II[ EUWriteToPBus3AB ].ORD ].b ← F;
p[ II[ UserMode2BA ].ORD ].b ← F;
p[ II[ DPCmdA ].ORD ].c ← 0;
p[ II[ DPRejectB ].ORD ].b ← F;
p[ II[ DPFaultB ].ORD ].c ← 0;
p[ II[ IPData ].ORD ].b ← F;
p[ II[ IPCmdFetchA ].ORD ].b ← F;
p[ II[ IPRejectB ].ORD ].b ← F;
p[ II[ IPFaultingB ].ORD ].b ← F;
p[ II[ DShA ].ORD ].b ← F;
p[ II[ DShB ].ORD ].b ← F;
p[ II[ DShRd ].ORD ].b ← F;
p[ II[ DShWt ].ORD ].b ← F;
p[ II[ DShIn ].ORD ].b ← F;
p[ II[ DShOut ].ORD ].b ← F;
p[ II[ ResetAB ].ORD ].b ← TRUE;
p[ II[ RescheduleAB ].ORD ].b ← F;
p[ II[ PhA ].ORD ].b ← F;
p[ II[ PhB ].ORD ].b ← F;
p[ II[ NotPhA ].ORD ].b ← F;
p[ II[ NotPhB ].ORD ].b ← TRUE;
FOR pass:
INT
IN [0..10)
DO
DoPass[pass, states, p, display];
IFUTest.ShowComplete[states] ENDLOOP;
Signal[]};
DoPass:
PROC [pass:
INT, states: StateSeq, p: Ports.Port, display: RosemaryUser.RoseDisplay] =
{FOR ph: QPh IN QPh DO DoQPh[ph, pass, states, p, display] ENDLOOP};
DoQPh:
PROC
[ph: QPh, pass: INT, states: StateSeq, p: Ports.Port, display: RosemaryUser.RoseDisplay] = {
time: INT ← 4*pass + (SELECT ph FROM A => 0, ab => 1, B => 2, ba => 3, ENDCASE => ERROR);
p[ II[ PhA ].ORD ].b ← ph = A;
p[ II[ NotPhA ].ORD ].b ← ph # A;
p[ II[ PhB ].ORD ].b ← ph = B;
p[ II[ NotPhB ].ORD ].b ← ph # B;
TerminalIO.WriteF["Pass %g %g %g\n",
IO.int[pass], IO.rope[QPhRope[ph]], IO.time[]];
RosemaryUser.LogSettle[display, time !
Rosemary.Stop => {
flatWire: CoreFlat.FlatWire ← NARROW[data];
name: ROPE ← CoreOps.GetShortWireName[flatWire.wire];
IF name.Length[]>0
THEN TerminalIO.WriteF["%g = X\n", IO.rope[name]]
ELSE TerminalIO.WriteRope["?????????? = X\n"]; RESUME}];
SELECT ph FROM A,B => IFUTest.UpdateStates[display.simulation, states, pass, ph]; ENDCASE;
RosemaryUser.UpdateDisplay[display];
IF PLASim.BadIns[] THEN TerminalIO.WriteRope["BadIns"]};
RosemaryUser.RegisterTestProc[formalTest, FormalTest];
simulation ← RosemaryUser.TestProcedureViewer[
cellType: cell,
testButtons: LIST[formalTest],
name: formalTest,
displayWires: RosemaryUser.DisplayCellTypePortLeafWires[cell],
flatten: TRUE,
cutSets: cuts]};