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. IFUTestComplete.mesa Copyright c 1986 by Xerox Corporation. All rights reserved. Last Edited by Curry, October 21, 1986 10:09:42 pm PDT Don Curry April 2, 1987 10:48:35 am PST Last Edited by: Louis Monier February 10, 1987 9:22:00 pm PST RosemaryUser.RegisterTestProc[formalTest, FormalTest]; simulation _ RosemaryUser.TestProcedureViewer[ cellType: cell, testButtons: LIST[formalTest], name: formalTest, displayWires: RosemaryUser.DisplayCellTypePortLeafWires[cell], flatten: TRUE, cutSets: cuts]}; ΚP˜šœ™Jšœ<™œ:˜ƒJ˜šΟnœœ˜Jšœ'œB˜rJšœ ˜Jš˜J˜Jšœœœ˜Jšœ œ˜!Jšœ œ ˜Jšœ œ˜$Jšœœ˜Jšžœœœœ(˜CJšžœœœ˜Jšœœ œ˜Jš œ œœ œ œ"˜TJ˜šž œœœ˜Jšœ˜Jšœ ˜ Jšœ˜Jšœ#˜#Jšœ œ˜!Jšœ6˜6Jšœ˜Jšžœœœ˜Jšœ6œ˜XJšœ  œ˜-Jšœœ˜$Jšœ1˜1šœ%˜%JšœH˜H—Jšœ'˜'Jšœ+˜+Jšœœ œ ˜Jšœœœ ˜ Jšœœœ ˜!Jšœœœ ˜#Jšœœœ ˜#Jšœœœ ˜$Jšœœœ ˜ Jšœœ œ ˜Jšœœœ ˜!Jšœœœ ˜ Jšœœœ ˜Jšœœœ ˜"Jšœœœ ˜!Jšœœœ ˜"Jšœœ œ ˜Jšœœ œ ˜Jšœœ œ ˜Jšœœ œ ˜Jšœœœ ˜Jšœœœ ˜Jšœœœœ˜"Jšœœœ ˜"Jšœœ œ ˜Jšœœ œ ˜šœœœ ˜Jšœ!˜!Jšœœ˜%—Jšœ ˜ —J˜šžœœœG˜^Jš œœ œœ%œ˜DJ˜—šžœ˜ JšœœI˜\Jš œœ œœ#œœ˜YJšœœ œ˜"Jšœœ œ˜"šœ$˜$Jšœ œœ ˜/—šœ'Οb œ˜9Jšœœ˜+Jšœœ+˜6šœ˜Jšœœ ˜/Jšœ)œ˜6——JšœœDœ˜ZJšœ$˜$Jšœœ˜6J˜—J™Jšœ6™6šœžœ™.Jšœ™Jšœœ™ Jšœ™Jšœ?™?Jšœ œ™Jšœ™——™šž œ˜%Jš žœœœžœœœ˜ Jšœœ œ ˜Jšœœœ ˜ Jšœœœ ˜!Jšœœœ ˜#Jšœœœ ˜#Jšœœœ ˜$Jšœœœ ˜ Jšœœ œ ˜Jšœœœ ˜!Jšœœœ ˜ Jšœœœ ˜Jšœœœ ˜"Jšœœœ ˜!Jšœœœ ˜"Jšœœ œ ˜Jšœœ œ ˜Jšœœ œ ˜Jšœœ œ ˜Jšœœœ ˜Jšœœœ ˜Jšœœœœ˜"Jšœœœ ˜"Jšœœ œœ˜ Jšœœ œ ˜Jšœ˜Jšœ Οc œ˜—J˜Jšœ˜—J˜—…—&„