[_CD4_]<datools7.0>Boole>FSAExample.mesa!2

FSAExample.mesa

Barth, November 3, 1986 12:36:05 pm PST

Bertrand Serlet April 2, 1987 9:40:21 pm PST

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.