<> <> <> <> <> <<>> DIRECTORY Core, CoreFlat, CoreOps, IFUTop, IFUPublic, IFUSim, IFUTest, IO, PLASim, Ports, Rope, Rosemary, RosemaryUser, TerminalIO; IFUTestComplete: CEDAR PROGRAM IMPORTS CoreFlat, CoreOps, IFUPublic, 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 = IFUTop.QPh; QPhRope: ARRAY QPh OF ROPE _ [A: "A", ab: "ab", B: "B", ba: "ba"]; Signal: SIGNAL = CODE; II: TYPE = IFUPublic.II; PortData: TYPE = RECORD [ name: ROPE, width: NAT _ 1, drive: Ports.Drive _ none ]; Formality: PUBLIC PROC = { states: StateSeq; simulation: Rosemary.Simulation; p: Ports.Port; display: RosemaryUser.RoseDisplay; formalTest: ROPE _ "FormalTest"; public: Core.Wire _ IFUPublic.IfuInitializedPublic[]; cell: CellType; F: BOOL _ FALSE; cuts: CoreFlat.CutSet _ CoreFlat.CreateCutSet[labels: LIST ["SimplePLA", "UpOneLevel"]]; cell _ IFUSim.FormalIFU[public, TRUE, FALSE]; 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[ EUAluOp ].ORD ].c _ 0; p[ II[ EUCondSel ].ORD ].c _ 0; p[ II[ EUCondition ].ORD ].b _ F; p[ II[ EURdFromPBus ].ORD ].b _ F; p[ II[ EUWriteToPBus ].ORD ].b _ F; p[ II[ UserMode ].ORD ].b _ F; p[ II[ DPCmd ].ORD ].c _ 0; p[ II[ DPReject ].ORD ].b _ F; p[ II[ DPFault ].ORD ].c _ 0; p[ II[ IPData ].ORD ].b _ F; p[ II[ IPCmdFetch ].ORD ].b _ F; p[ II[ IPReject ].ORD ].b _ F; p[ II[ IPFaulting ].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[ Reset ].ORD ].b _ TRUE; p[ II[ Reschedule ].ORD ].b _ F; p[ II[ PhA ].ORD ].b _ F; p[ II[ PhB ].ORD ].b _ F; 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[ PhB ].ORD ].b _ ph = B; TerminalIO.PutF["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.PutF["%g = X\n", IO.rope[name]] ELSE TerminalIO.PutRope["?????????? = X\n"]; RESUME}]; SELECT ph FROM A,B => IFUTest.UpdateStates[display.simulation, states, pass, ph]; ENDCASE; RosemaryUser.UpdateDisplay[display]; IF PLASim.BadIns[] THEN TerminalIO.PutRope["BadIns"]}; <<>> <> <> <> <> <> <> <> <> <<>> FormalTest: RosemaryUser.TestProc = { T: BOOL = TRUE; F: BOOL = FALSE; p[ II[ KBus ].ORD ].lc _ 0; p[ II[ EUAluOp ].ORD ].c _ 0; p[ II[ EUCondSel ].ORD ].c _ 0; p[ II[ EUCondition ].ORD ].b _ F; p[ II[ EURdFromPBus ].ORD ].b _ F; p[ II[ EUWriteToPBus ].ORD ].b _ F; p[ II[ UserMode ].ORD ].b _ F; p[ II[ DPCmd ].ORD ].c _ 0; p[ II[ DPReject ].ORD ].b _ F; p[ II[ DPFault ].ORD ].c _ 0; p[ II[ IPData ].ORD ].b _ F; p[ II[ IPCmdFetch ].ORD ].b _ F; p[ II[ IPReject ].ORD ].b _ F; p[ II[ IPFaulting ].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[ Reset ].ORD ].b _ TRUE; p[ II[ Reschedule ].ORD ].b _ F; p[ II[ PhA ].ORD ].b _ TRUE; p[ II[ PhB ].ORD ].b _ F; Eval[]; Signal[] -- Whew! -- }; END.