<> <> <> <> <<>> DIRECTORY Core, CoreCreate, CoreFlat, CoreOps, IFU2, IFUSim, IFUTest, IO, PLASim, Ports, Rope, Rosemary, RosemaryUser, TerminalIO; 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"]}; <<>> <> <> <> <> <> <> <> <> <<>> FormalTest: RosemaryUser.TestProc = { T: BOOL = TRUE; F: BOOL = FALSE; 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 _ TRUE; p[ II[ PhB ].ORD ].b _ F; p[ II[ NotPhA ].ORD ].b _ F; p[ II[ NotPhB ].ORD ].b _ TRUE; Eval[]; Signal[] -- Whew! -- }; END.