DIRECTORY Boole, CoreCreate, CoreFlat, CoreOps, FiniteStateAutomata, Ports, Rosemary, RosemaryUser; FSAExample: CEDAR PROGRAM IMPORTS Boole, CoreCreate, CoreFlat, CoreOps, FiniteStateAutomata, Ports, Rosemary, RosemaryUser = BEGIN OPEN Boole, CoreCreate, FiniteStateAutomata; Vdd, Gnd, Clock, Reset, DA, RB, WB, WS, BIOW, IOR, Ref, RASPChg, TwoReqPend, ReadDone, WriteDone, DlyDone, RefDone, LatchCAdd, Unload, StartA, LatchRAdd, Post5Cyc, Post2Cyc, SWWPort, RASPChgOut, LatchWD0, LatchWD1, LatchWD2, LatchWD3, Write, LatchRData, IOCmd, Refresh: NAT; CreateFSA: PROC RETURNS [ct: CellType] = { fsa: StateMachine; states: LIST OF ATOM _ LIST[$Idle, $Decode, $IOR0]; DA: Wire _ CoreOps.CreateWire[name: "DA"]; RB: Wire _ CoreOps.CreateWire[name: "RB"]; WB: Wire _ CoreOps.CreateWire[name: "WB"]; WS: Wire _ CoreOps.CreateWire[name: "WS"]; BIOW: Wire _ CoreOps.CreateWire[name: "BIOW"]; IOR: Wire _ CoreOps.CreateWire[name: "IOR"]; Ref: Wire _ CoreOps.CreateWire[name: "Ref"]; RASPChg: Wire _ CoreOps.CreateWire[name: "RASPChg"]; TwoReqPend: Wire _ CoreOps.CreateWire[name: "TwoReqPend"]; ReadDone: Wire _ CoreOps.CreateWire[name: "ReadDone"]; WriteDone: Wire _ CoreOps.CreateWire[name: "WriteDone"]; DlyDone: Wire _ CoreOps.CreateWire[name: "DlyDone"]; RefDone: Wire _ CoreOps.CreateWire[name: "RefDone"]; LatchCAdd: Wire _ CoreOps.CreateWire[name: "LatchCAdd"]; Unload: Wire _ CoreOps.CreateWire[name: "Unload"]; StartA: Wire _ CoreOps.CreateWire[name: "StartA"]; LatchRAdd: Wire _ CoreOps.CreateWire[name: "LatchRAdd"]; Post5Cyc: Wire _ CoreOps.CreateWire[name: "Post5Cyc"]; Post2Cyc: Wire _ CoreOps.CreateWire[name: "Post2Cyc"]; SWWPort: Wire _ CoreOps.CreateWire[name: "SWWPort"]; RASPChgOut: Wire _ CoreOps.CreateWire[name: "RASPChgOut"]; LatchWD0: Wire _ CoreOps.CreateWire[name: "LatchWD0"]; LatchWD1: Wire _ CoreOps.CreateWire[name: "LatchWD1"]; LatchWD2: Wire _ CoreOps.CreateWire[name: "LatchWD2"]; LatchWD3: Wire _ CoreOps.CreateWire[name: "LatchWD3"]; Write: Wire _ CoreOps.CreateWire[name: "Write"]; LatchRData: Wire _ CoreOps.CreateWire[name: "LatchRData"]; IOCmd: Wire _ CoreOps.CreateWire[name: "IOCmd"]; Refresh: Wire _ CoreOps.CreateWire[name: "Refresh"]; public: Wire _ WireList[LIST["Vdd", "Gnd", "Clock", "Reset", DA, RB, WB, WS, BIOW, IOR, Ref, RASPChg, TwoReqPend, ReadDone, WriteDone, DlyDone, RefDone, LatchCAdd, Unload, StartA, LatchRAdd, Post5Cyc, Post2Cyc, SWWPort, RASPChgOut, LatchWD0, LatchWD1, LatchWD2, LatchWD3, Write, LatchRData, IOCmd, Refresh]]; states _ StateSeq[states, "RB", 8]; states _ StateSeq[states, "WB", 6]; states _ StateSeq[states, "WSIOW", 2]; states _ StateSeq[states, "Ref", 3]; fsa _ NewMachine[states]; Mealy[fsa, $Idle, LIST[LatchCAdd, Unload], LIST [ [$Idle, Not[DA]], [$Decode, DA]]]; Mealy[fsa, $Decode, NIL, LIST [ [$Decode, Or[RASPChg, TwoReqPend]], [$RB0, And[RB, Not[Ref], Not[RASPChg]]], [$WB0, And[WB, Not[Ref], Not[RASPChg]]], [$WSIOW0, And[Or[WS, BIOW], Not[Ref]]], [$IOR0, And[IOR, Not[Ref]]], [$Ref0, And[Ref, Not[RASPChg]]]]]; Mealy[fsa, $RB0, LIST[StartA, LatchRAdd], LIST[[$RB1, true]]]; Mealy[fsa, $RB1, NIL, LIST[[$RB1, Not[ReadDone]], [$RB2, ReadDone]]]; Mealy[fsa, $RB2, LIST[Post5Cyc], LIST[[$RB3, true]]]; Mealy[fsa, $RB3, NIL, LIST[[$RB4, true]]]; Mealy[fsa, $RB4, NIL, LIST[[$RB5, true]]]; Mealy[fsa, $RB5, NIL, LIST[[$RB6, true]]]; Mealy[fsa, $RB6, NIL, LIST[[$RB7, true]]]; Mealy[fsa, $RB7, LIST[SWWPort, RASPChgOut], LIST[[$Idle, true]]]; Mealy[fsa, $WB0, LIST[LatchWD0, Post2Cyc, Unload, LatchRAdd, SWWPort], LIST[[$WB1, true]]]; Mealy[fsa, $WB1, LIST[LatchWD1, Unload], LIST[[$WB2, true]]]; Mealy[fsa, $WB2, LIST[LatchWD2, Unload], LIST[[$WB3, true]]]; Mealy[fsa, $WB3, LIST[LatchWD3, Unload, Write, StartA], LIST[[$WB4, true]]]; Mealy[fsa, $WB4, NIL, LIST[[$WB4, Not[WriteDone]], [$WB5, WriteDone]]]; Mealy[fsa, $WB5, LIST[RASPChgOut], LIST[[$Idle, true]]]; Mealy[fsa, $WSIOW0, LIST[LatchCAdd, Unload, Post2Cyc, LatchRAdd], LIST[[$WSIOW1, true]]]; Mealy[fsa, $WSIOW1, LIST[LatchRData], LIST[[$Idle, true]]]; Mealy[fsa, $IOR0, LIST[Post2Cyc, LatchRAdd, IOCmd, LatchRData], LIST[[$Idle, true]]]; Mealy[fsa, $Ref0, LIST[StartA, Refresh], LIST[[$Ref1, true]]]; Mealy[fsa, $Ref1, LIST[Refresh], LIST[[$Ref1, RefDone], [$Ref2, DlyDone]]]; Mealy[fsa, $Ref2, LIST[RASPChgOut], LIST[[$Decode, true]]]; fsa.initialState _ FindState[fsa, $Idle]; ct _ StateMachineCell[public: public, fsa: fsa, name: "TestFSA", completeCheck: TRUE, assert: AndList[LIST[ OrList[LIST[Ref, RB, WB, WS, BIOW, IOR, RASPChg, TwoReqPend]], OrList[LIST[RefDone, DlyDone]], Not[OrList[LIST[ And[Ref, TwoReqPend], And[RB, Or[RASPChg, TwoReqPend]], And[RB, WB], And[RB, Or[WS, BIOW]], And[RB, IOR], And[WB, Or[RASPChg, TwoReqPend]], And[WB, Or[WS, BIOW]], And[WB, IOR], And[Or[WS, BIOW], Or[RASPChg, TwoReqPend]], And[Or[WS, BIOW], IOR], And[IOR, Or[RASPChg, TwoReqPend]], And[RefDone, DlyDone]]]]]]]; }; Init: PROC = { ct: CoreCreate.CellType _ CreateFSA[]; InitPortIndicies[ct]; [] _ Rosemary.SetFixedWire[ct.public[Vdd], H]; [] _ Rosemary.SetFixedWire[ct.public[Gnd], L]; [] _ RosemaryUser.TestProcedureViewer[name: "FSA Tester", cellType: ct, testButtons: LIST["TestFSA"], displayWires: RosemaryUser.DisplayPortLeafWires[ct], cutSet: CoreFlat.CreateCutSet[labels: LIST["FSA"]]]; }; InitPortIndicies: PROC [ct: CoreCreate.CellType] = { [Vdd, Gnd, Clock, Reset] _ Ports.PortIndexes[ct.public, "Vdd", "Gnd", "Clock", "Reset"]; [DA, RB, WB, WS, BIOW, IOR, Ref, RASPChg, TwoReqPend, ReadDone] _ Ports.PortIndexes[ct.public, "DA", "RB", "WB", "WS", "BIOW", "IOR", "Ref", "RASPChg", "TwoReqPend", "ReadDone"]; [WriteDone, DlyDone, RefDone, LatchCAdd, Unload, StartA, LatchRAdd, Post5Cyc, Post2Cyc, SWWPort] _ Ports.PortIndexes[ct.public, "WriteDone", "DlyDone", "RefDone", "LatchCAdd", "Unload", "StartA", "LatchRAdd", "Post5Cyc", "Post2Cyc", "SWWPort"]; [RASPChgOut, LatchWD0, LatchWD1, LatchWD2, LatchWD3, Write, LatchRData, IOCmd, Refresh] _ Ports.PortIndexes[ct.public, "RASPChgOut", "LatchWD0", "LatchWD1", "LatchWD2", "LatchWD3", "Write", "LatchRData", "IOCmd", "Refresh"]; }; TestFSA: RosemaryUser.TestProc = { InitPortIndicies[cellType]; p[DA].d _ force; p[DA].l _ L; p[RB].d _ force; p[RB].l _ L; p[WB].d _ force; p[WB].l _ L; p[WS].d _ force; p[WS].l _ L; p[BIOW].d _ force; p[BIOW].l _ L; p[IOR].d _ force; p[IOR].l _ L; p[Ref].d _ force; p[Ref].l _ L; p[RASPChg].d _ force; p[RASPChg].l _ L; p[TwoReqPend].d _ force; p[TwoReqPend].l _ L; p[ReadDone].d _ force; p[ReadDone].l _ L; p[WriteDone].d _ force; p[WriteDone].l _ L; p[DlyDone].d _ force; p[DlyDone].l _ L; p[RefDone].d _ force; p[RefDone].l _ L; p[Reset].d _ force; p[Reset].l _ H; p[Clock].d _ force; p[Clock].l _ L; Eval[]; -- setup p[Reset].l _ L; p[Clock].l _ H; Eval[]; -- reset to Idle p[Clock].l _ L; Eval[]; p[LatchCAdd].d _ expect; p[LatchCAdd].l _ H; p[Unload].d _ expect; p[Unload].l _ H; p[StartA].d _ expect; p[StartA].l _ L; p[LatchRAdd].d _ expect; p[LatchRAdd].l _ L; p[Post5Cyc].d _ expect; p[Post5Cyc].l _ L; p[Post2Cyc].d _ expect; p[Post2Cyc].l _ L; p[SWWPort].d _ expect; p[SWWPort].l _ L; p[RASPChgOut].d _ expect; p[RASPChgOut].l _ L; p[LatchWD0].d _ expect; p[LatchWD0].l _ L; p[LatchWD1].d _ expect; p[LatchWD1].l _ L; p[LatchWD2].d _ expect; p[LatchWD2].l _ L; p[LatchWD3].d _ expect; p[LatchWD3].l _ L; p[Write].d _ expect; p[Write].l _ L; p[LatchRData].d _ expect; p[LatchRData].l _ L; p[IOCmd].d _ expect; p[IOCmd].l _ L; p[Refresh].d _ expect; p[Refresh].l _ L; p[Clock].l _ H; Eval[]; -- Idle p[DA].l _ H; p[Clock].l _ L; Eval[]; p[DA].l _ L; p[LatchCAdd].l _ L; p[Unload].l _ L; p[Clock].l _ H; Eval[]; -- Decode p[RB].l _ H; p[Clock].l _ L; Eval[]; p[RB].l _ L; p[StartA].l _ H; p[LatchRAdd].l _ H; p[Clock].l _ H; Eval[]; -- RB0 }; RosemaryUser.RegisterTestProc["TestFSA", TestFSA]; END. °FSAExample.mesa Copyright س 1986, 1987 by Xerox Corporation. All rights reserved. Barth, November 3, 1986 12:36:05 pm PST Bertrand Serlet April 2, 1987 9:40:21 pm PST ‌تw– "cedar" styleکcodeڑœ™KڑœB™BK™'K™,K™—Kڑدk œ[کdJک•StartOfExpansion[]ڑدn œ‌œ‌کKڑ‌œ\کcKڑ‌œ‌œ(ک2—KکJڑœژ‌œک’Jکڑ‍ œ‌œ‌œک*JڑœکJڑ œ‌œ‌œ‌œ‌œک3JکJڑœ*ک*Jڑœ*ک*Jڑœ*ک*Jڑœ*ک*Jڑœ.ک.Jڑœ,ک,Jڑœ,ک,Jڑœ4ک4Jڑœ:ک:Jڑœ6ک6Jڑœ8ک8Jڑœ4ک4Jڑœ4ک4Jڑœ8ک8Jڑœ2ک2Jڑœ2ک2Jڑœ8ک8Jڑœ6ک6Jڑœ6ک6Jڑœ4ک4Jڑœ:ک:Jڑœ6ک6Jڑœ6ک6Jڑœ6ک6Jڑœ6ک6Jڑœ0ک0Jڑœ:ک:Jڑœ0ک0Jڑœ4ک4Jکڑœ‌œ کKڑœ‌œ‌œ+کEKڑœ‌œ‌œک5Kڑœ‌œ‌œک*Kڑœ‌œ‌œک*Kڑœ‌œ‌œک*Kڑœ‌œ‌œک*Kڑœ‌œ‌œکAKڑœ‌œ1‌œک[Kڑœ‌œ‌œک=Kڑœ‌œ‌œک=Kڑœ‌œ#‌œکLKڑœ‌œ‌œ-کGKڑœ‌œ‌œک8Kڑœ‌œ*‌œکYKڑœ‌œ‌œک;Kڑœ‌œ*‌œکUKڑœ‌œ‌œک>Kڑœ‌œ‌œ&کKKڑœ‌œ‌œک;KکKڑœ)ک)ڑœP‌œ‌œکkKڑœ‌œ3ک>Kڑœ‌œکڑœ‌œکKڑœکKڑœ!ک!KڑœکKڑœکKڑœ ک Kڑœ!ک!KڑœکKڑœ ک Kڑœ+ک+KڑœکKڑœ"ک"Kڑœک——KکKک—ڑ‍œ‌œکKک&KڑœکKکKڑœ.ک.Kڑœ.ک.KکKڑœU‌œh‌œ کدKکKک—ڑ‍œ‌œک4KڑœXکXKڑ œ‌œ‌œ‌œ‌œ‌œ‌œکک²KڑœôکôKڑœàکàKکKک—ڑ‍œک"KڑœکKکKڑœکKڑœکKڑœکKڑœکKڑœ!ک!KڑœکKڑœکKڑœ'ک'Kڑœ-ک-Kڑœ)ک)Kڑœ+ک+Kڑœ'ک'Kڑœ'ک'KکKڑœ#ک#Kڑœ#ک#Kڑœ دcکKکKکKڑœکKڑœکKڑœ ںکKکKڑœکKڑœکKکKڑœ,ک,Kڑœ&ک&Kڑœ&ک&Kڑœ,ک,Kڑœ*ک*Kڑœ*ک*Kڑœ(ک(Kڑœ.ک.Kڑœ*ک*Kڑœ*ک*Kڑœ*ک*Kڑœ*ک*Kڑœ$ک$Kڑœ.ک.Kڑœ$ک$Kڑœ(ک(KڑœکKڑœ ںکKکKڑœکKڑœکKڑœکKکKڑœکKڑœکKڑœکKڑœکKڑœ ں کKکKڑœکKڑœکKڑœکKکKڑœکKڑœکKڑœکKڑœکKڑœ ںکKڑœکKک—ڑœ2ک2Kک—Kڑ‌œکKک—…—Z%پ