<> <> <> <> <<>> DIRECTORY Atom, BrineIO, Boole, Core, CoreFlat, CoreIO, CoreOps, FiniteStateAutomata, RefTab, IO, Ports, Rope, Rosemary, TerminalIO; FiniteStateAutomataImpl: CEDAR PROGRAM IMPORTS Atom, BrineIO, Boole, CoreFlat, CoreIO, CoreOps, RefTab, IO, Ports, Rope, Rosemary, TerminalIO EXPORTS FiniteStateAutomata = BEGIN OPEN FiniteStateAutomata; <> CreateError: PUBLIC SIGNAL [msg: ROPE] = CODE; NewMachine: PUBLIC PROC [states: LIST OF ATOM] RETURNS [fsa: StateMachine] = { fsa _ NEW[StateMachineRec]; FOR s: LIST OF ATOM _ states, s.rest UNTIL s=NIL DO fsa.states _ CONS[NEW[StateRec _ [name: s.first]], fsa.states]; ENDLOOP; }; NewTransition: PUBLIC PROC [fsa: StateMachine, from, to: ATOM, expr: Expression] = { fromState: State _ FindState[fsa, from]; toState: State _ FindState[fsa, to]; fromState.transitions _ CONS[NEW[TransitionRec _ [expr, toState]], fromState.transitions]; }; NewTransitions: PUBLIC PROC [fsa: StateMachine, from: ATOM, transitions: TransitionLiterals] = { FOR t: TransitionLiterals _ transitions, t.rest UNTIL t=NIL DO NewTransition[fsa, from, t.first.to, t.first.expr]; ENDLOOP; }; FindState: PUBLIC PROC [fsa: StateMachine, state: ATOM] RETURNS [stateRef: State] = { FOR s: States _ fsa.states, s.rest UNTIL s=NIL DO IF s.first.name=state THEN { stateRef _ s.first; EXIT; }; REPEAT FINISHED => ERROR CreateError[Rope.Cat["Can't find state ", Atom.GetPName[state]]]; ENDLOOP; }; StateSeq: PUBLIC PROC [states: LIST OF ATOM, root: ROPE, count: NAT] RETURNS [newStates: LIST OF ATOM] = { newStates _ states; FOR i: NAT IN [0..count) DO newStates _ CONS[Atom.MakeAtom[IO.PutFR["%g%g", IO.rope[root], IO.card[i]]], newStates]; ENDLOOP; }; <> <> < WITH wr2 SELECT FROM>> < w1=w2,>> < Rope.Equal[CoreOps.GetShortWireName[w1], r2],>> < Rope.Equal[CoreOps.GetShortWireName[w1], Rope.FromRefText[t2]],>> < ERROR,>> < WITH wr2 SELECT FROM>> < Rope.Equal[r1, CoreOps.GetShortWireName[w2]],>> < Rope.Equal[r1, r2],>> < Rope.Equal[r1, Rope.FromRefText[t2]],>> < ERROR,>> < WITH wr2 SELECT FROM>> < Rope.Equal[Rope.FromRefText[t1], CoreOps.GetShortWireName[w2]],>> < Rope.Equal[Rope.FromRefText[t1], r2],>> < Rope.Equal[Rope.FromRefText[t1], Rope.FromRefText[t2]],>> < ERROR,>> < ERROR;>> <<};>> <<>> Mealy: PUBLIC PROC [fsa: StateMachine, state: ATOM, outputs: LIST OF Core.Wire, transitions: TransitionLiterals] = { statePtr: State _ FindState[fsa, state]; NewTransitions[fsa, state, transitions]; FOR o: LIST OF Core.Wire _ outputs, o.rest UNTIL o=NIL DO FOR out: Outputs _ fsa.outputs, out.rest UNTIL out=NIL DO IF o.first=out.first.output THEN { out.first.expr _ Boole.Or[out.first.expr, statePtr]; EXIT; }; REPEAT FINISHED => fsa.outputs _ CONS[[output: o.first, expr: statePtr], fsa.outputs]; ENDLOOP; ENDLOOP; }; <> fsaClass: Core.CellClass _ CoreIO.RegisterClass[ Rosemary.BindCellClass[NEW [Core.CellClassRec _ [name: "FSA", recast: RecastFSA, layersProps: FALSE]], Rosemary.Register["FSARoseClass", InitFSA, EvalFSA]], WriteFSA, ReadFSA]; <<>> WriteFSA: CoreIO.ClassWriteProc = { WriteExpression: PROC [expr: Boole.Expression] = { WriteVariable: PROC [out: Core.STREAM, var: Boole.Variable] = { WITH var SELECT FROM w: Core.Wire => { BrineIO.WriteID[stream, "w"]; CoreIO.WriteWire[stream, wireIDTable, w]; }; s: State => { BrineIO.WriteID[stream, "s"]; BrineIO.WriteAtom[stream, s.name]; }; ENDCASE => ERROR; }; Boole.PutExpr[out: stream, expr: expr, putRefAny: WriteVariable]; BrineIO.WriteID[stream, NIL]; }; fsa: StateMachine _ NARROW[cellType.data]; count: INT _ 0; FOR sl: States _ fsa.states, sl.rest UNTIL sl=NIL DO count _ count + 1; ENDLOOP; BrineIO.WriteInt[stream, count]; FOR sl: States _ fsa.states, sl.rest UNTIL sl=NIL DO IF sl.first.name=NIL THEN ERROR; BrineIO.WriteAtom[stream, sl.first.name]; ENDLOOP; FOR sl: States _ fsa.states, sl.rest UNTIL sl=NIL DO count _ 0; FOR tl: Transitions _ sl.first.transitions, tl.rest UNTIL tl=NIL DO count _ count + 1; ENDLOOP; BrineIO.WriteInt[stream, count]; FOR tl: Transitions _ sl.first.transitions, tl.rest UNTIL tl=NIL DO WriteExpression[tl.first.expr]; BrineIO.WriteAtom[stream, tl.first.target.name]; ENDLOOP; ENDLOOP; count _ 0; FOR ol: Outputs _ fsa.outputs, ol.rest UNTIL ol=NIL DO count _ count + 1; ENDLOOP; BrineIO.WriteInt[stream, count]; FOR ol: Outputs _ fsa.outputs, ol.rest UNTIL ol=NIL DO CoreIO.WriteWire[stream, wireIDTable, ol.first.output]; WriteExpression[ol.first.expr]; ENDLOOP; BrineIO.WriteAtom[stream, fsa.initialState.name]; }; <<>> ReadFSA: CoreIO.ClassReadProc = { ReadExpression: PROC RETURNS [expr: Boole.Expression] = { ReadVariable: PROC [in: Core.STREAM] RETURNS [var: Boole.Variable] = { type: ROPE _ BrineIO.ReadID[stream]; var _ SELECT TRUE FROM Rope.Equal["w", type] => CoreIO.ReadWire[stream, wireIDTable], Rope.Equal["s", type] => FindState[fsa, BrineIO.ReadAtom[stream]], ENDCASE => ERROR; }; expr _ Boole.GetExpr[in: stream, getRefAny: ReadVariable]; }; fsa: StateMachine; count: INT _ BrineIO.ReadInt[stream]; states: LIST OF ATOM _ NIL; FOR sc: INT IN [0..count) DO states _ CONS[BrineIO.ReadAtom[stream], states]; ENDLOOP; fsa _ NewMachine[states]; FOR sl: States _ fsa.states, sl.rest UNTIL sl=NIL DO count: INT _ BrineIO.ReadInt[stream]; FOR tc: INT IN [0..count) DO expr: Boole.Expression _ ReadExpression[]; target: ATOM _ BrineIO.ReadAtom[stream]; NewTransition[fsa, sl.first.name, target, expr]; ENDLOOP; ENDLOOP; count _ BrineIO.ReadInt[stream]; FOR oc: INT IN [0..count) DO wire: Core.Wire _ CoreIO.ReadWire[stream, wireIDTable]; expr: Boole.Expression _ ReadExpression[]; fsa.outputs _ CONS[[wire, expr], fsa.outputs]; ENDLOOP; fsa.initialState _ FindState[fsa, BrineIO.ReadAtom[stream]]; cellType.data _ fsa; }; <<>> FSAState: TYPE = REF FSAStateRec; FSAStateRec: TYPE = RECORD [ fsa: StateMachine _ NIL, lastClock: Ports.Level _ X, masterReset: Ports.Level _ X, masterState: State _ NIL, slaveState: State _ NIL, masterOutputs: Ports.LevelSequence _ NIL, slaveOutputs: Ports.LevelSequence _ NIL, resetPort: NAT _ 0, clockPort: NAT _ 0, ioPorts: RefTab.Ref _ NIL, outputPorts: SEQUENCE size: NAT OF Ports.Port]; InitFSA: Rosemary.InitProc = { BindIO: Ports.EachWirePortPairProc = { IF port.levelType#composite THEN { IF port.levelType#l THEN ERROR; [] _ RefTab.Insert[state.ioPorts, wire, port] }; }; state: FSAState; fsa: StateMachine _ NARROW[cellType.data]; ffOut: NAT _ 0; FOR outs: Outputs _ fsa.outputs, outs.rest UNTIL outs=NIL DO ffOut _ ffOut + 1; ENDLOOP; state _ NEW[FSAStateRec[ffOut]]; state.fsa _ fsa; state.masterOutputs _ NEW[Ports.LevelSequenceRec[ffOut]]; state.slaveOutputs _ NEW[Ports.LevelSequenceRec[ffOut]]; FOR i: NAT IN [0..ffOut) DO state.masterOutputs[i] _ state.slaveOutputs[i] _ X; ENDLOOP; state.resetPort _ Ports.PortIndex[cellType.public, "Reset"]; state.clockPort _ Ports.PortIndex[cellType.public, "Clock"]; state.ioPorts _ RefTab.Create[]; IF Ports.VisitBinding[cellType.public, p, BindIO] THEN ERROR; ffOut _ 0; FOR outs: Outputs _ fsa.outputs, outs.rest UNTIL outs=NIL DO state.outputPorts[ffOut] _ NARROW[RefTab.Fetch[state.ioPorts, outs.first.output].val]; state.outputPorts[ffOut].d _ drive; ffOut _ ffOut + 1; ENDLOOP; IF ffOut#state.size THEN ERROR; stateAny _ state; }; EvalFSA: Rosemary.EvalProc = { EvalStateOrWire: PROC [var: Boole.Variable] RETURNS [expr: Expression] = { WITH var SELECT FROM s: State => expr _ SELECT TRUE FROM state.masterReset=H => IF s=fsa.initialState THEN Boole.true ELSE Boole.false, state.masterState=NIL => NIL, s=state.masterState => Boole.true, ENDCASE => Boole.false; w: Core.Wire => { p: Ports.Port _ NARROW[RefTab.Fetch[state.ioPorts, w].val]; expr _ SELECT p.l FROM L => Boole.false, H => Boole.true, X => NIL, ENDCASE => ERROR; }; ENDCASE => ERROR; }; EvalExpr: PROC [expr: Expression] RETURNS [level: Ports.Level] = { level _ SELECT Boole.FullEval[expr, EvalStateOrWire] FROM NIL => X, Boole.true => H, Boole.false => L ENDCASE => ERROR; }; state: FSAState _ NARROW[stateAny]; fsa: StateMachine _ state.fsa; SELECT TRUE FROM p[state.clockPort].l=L => { outs: Outputs _ fsa.outputs; state.masterReset _ p[state.resetPort].l; state.masterState _ NIL; IF state.slaveState#NIL AND state.masterReset=L THEN { FOR trans: Transitions _ state.slaveState.transitions, trans.rest UNTIL trans=NIL DO transVal: Ports.Level _ EvalExpr[trans.first.expr]; SELECT TRUE FROM transVal=X OR (transVal=H AND state.masterState#NIL AND state.masterState#trans.first.target) => { state.masterState _ NIL; EXIT; }; transVal=H => state.masterState _ trans.first.target; ENDCASE; ENDLOOP; }; FOR out: NAT IN [0..state.masterOutputs.size) DO state.masterOutputs[out] _ EvalExpr[outs.first.expr]; outs _ outs.rest; ENDLOOP; }; state.lastClock=L AND p[state.clockPort].l=H => { FOR out: NAT IN [0..state.slaveOutputs.size) DO state.slaveOutputs[out] _ state.masterOutputs[out]; ENDLOOP; state.slaveState _ SELECT state.masterReset FROM H => fsa.initialState, L => state.masterState, X => NIL, ENDCASE => ERROR; }; ENDCASE; FOR out: NAT IN [0..state.slaveOutputs.size) DO state.outputPorts[out].l _ state.slaveOutputs[out]; ENDLOOP; state.lastClock _ p[state.clockPort].l; }; RecastFSA: Core.RecastProc = { ERROR; }; StateMachineCell: PUBLIC PROC [public: Core.Wire, fsa: StateMachine, name: ROPE _ NIL, props: Core.Properties _ NIL, completeCheck: BOOL _ FALSE, assert: Boole.Expression _ Boole.true] RETURNS [cellType: Core.CellType] = { CheckPublic: PROC [var: Boole.Variable] = { IF NOT ISTYPE[var, Core.Wire] THEN SIGNAL CreateError["Some transition variable is not a wire"]; IF NOT CoreOps.RecursiveMember[public, NARROW[var]] THEN SIGNAL CreateError["Some wire variable is not a member of the public"]; }; CheckStateOrPublic: PROC [var: Boole.Variable] = { WITH var SELECT FROM s: State => FOR states: States _ fsa.states, states.rest UNTIL states=NIL DO IF s=states.first THEN EXIT; REPEAT FINISHED => SIGNAL CreateError["Some expression state is not a state of the state machine"]; ENDLOOP; w: Core.Wire => CheckPublic[var]; ENDCASE => SIGNAL CreateError["Some variable is not a state or public wire"]; }; SetL: PROC [wire: Core.Wire] = {[] _ Ports.InitPort[wire, l]}; targetStates: RefTab.Ref _ RefTab.Create[]; CoreOps.VisitRootAtomics[public, SetL]; cellType _ CoreOps.CreateCellType[class: fsaClass, public: public, data: fsa, name: name, props: props]; [] _ CoreFlat.CellTypeCutLabels[cellType, "FSA"]; IF CoreOps.GetWireIndex[cellType.public, "Reset"]<0 THEN SIGNAL CreateError["Cannot find Reset in public"]; IF CoreOps.GetWireIndex[cellType.public, "Clock"]<0 THEN SIGNAL CreateError["Cannot find Clock in public"]; FOR outs: Outputs _ fsa.outputs, outs.rest UNTIL outs=NIL DO IF NOT CoreOps.RecursiveMember[public, outs.first.output] THEN SIGNAL CreateError["Some output is not a member of the public"]; Boole.EnumerateVars[outs.first.expr, CheckStateOrPublic]; ENDLOOP; FOR states: States _ fsa.states, states.rest UNTIL states=NIL DO IF states.first.transitions=NIL THEN SIGNAL CreateError["Some state is not a source state"]; FOR trans: Transitions _ states.first.transitions, trans.rest UNTIL trans=NIL DO Boole.EnumerateVars[trans.first.expr, CheckPublic]; [] _ RefTab.Insert[targetStates, trans.first.target, $Target]; ENDLOOP; ENDLOOP; FOR states: States _ fsa.states, states.rest UNTIL states=NIL DO IF RefTab.Fetch[targetStates, states.first].val=NIL AND states.first#fsa.initialState THEN SIGNAL CreateError["Some state is not a target state"]; ENDLOOP; IF completeCheck THEN ValidateFSA[CoreOps.InheritCellTypeName[cellType], fsa, assert]; }; <<>> ValidateFSA: PROC [name: ROPE, fsa: StateMachine, assert: Expression _ Boole.true] ~ { FOR states: States _ fsa.states, states.rest WHILE states#NIL DO from: State = states.first; all: Expression _ Boole.Not[assert]; FOR transitions: Transitions _ from.transitions, transitions.rest WHILE transitions#NIL DO e1: Expression = transitions.first.expr; s1: State = transitions.first.target; all _ Boole.Or[all, e1]; FOR others: Transitions _ transitions.rest, others.rest WHILE others#NIL DO e2: Expression = others.first.expr; s2: State = others.first.target; IF ~Boole.Equal[Boole.And[e1, e2, assert], Boole.false] THEN { TerminalIO.PutF["Conflicting transition from %g to %g and %g because %g is not FALSE in cell type %g\n", IO.atom[from.name], IO.atom[s1.name], IO.atom[s2.name], IO.rope[FSAExprToRope[Boole.Not[Boole.And[e1, e2, assert]]]], IO.rope[name]]; SIGNAL CreateError["See terminal"]; }; ENDLOOP; ENDLOOP; IF ~Boole.Equal[all, Boole.true] THEN { TerminalIO.PutF["Transitions from %g do not cover all cases because %g is not TRUE in cell type %g\n", IO.atom[from.name], IO.rope[FSAExprToRope[all]], IO.rope[name]]; SIGNAL CreateError["See terminal"]; }; ENDLOOP; }; FSAExprToRope: PROC [expr: Expression] RETURNS [ROPE] = { PrintVar: PROC [out: IO.STREAM, var: Boole.Variable] ~ { out.Put1[WITH var SELECT FROM w: Core.Wire => IO.rope[CoreOps.GetShortWireName[w]], s: State => IO.atom[s.name], ENDCASE => IO.rope["???"] ]; }; out: IO.STREAM _ IO.ROS[]; Boole.PutExpr[out: out, expr: expr, putRefAny: PrintVar]; RETURN [IO.RopeFromROS[out]]; }; END.