FiniteStateAutomataImpl.mesa
Copyright Ó 1986, 1987 by Xerox Corporation. All rights reserved.
Barth, April 1, 1987 11:19:41 am PST
Bertrand Serlet April 2, 1987 9:39:30 pm PST
DIRECTORY Atom, Boole, Core, CoreFlat, CoreIO, CoreOps, FiniteStateAutomata, RefTab, IO, Ports, Rope, Rosemary, TerminalIO;
FiniteStateAutomataImpl: CEDAR PROGRAM
IMPORTS Atom, Boole, CoreFlat, CoreIO, CoreOps, RefTab, IO, Ports, Rope, Rosemary, TerminalIO
EXPORTS FiniteStateAutomata
= BEGIN OPEN FiniteStateAutomata;
Creation
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;
};
WREqual: PROC [wr1, wr2: CoreCreate.WR] RETURNS [yes: BOOL] = {
yes ← WITH wr1 SELECT FROM
w1: CoreCreate.Wire => WITH wr2 SELECT FROM
w2: CoreCreate.Wire => w1=w2,
r2: ROPE => Rope.Equal[CoreOps.GetShortWireName[w1], r2],
t2: REF TEXT => Rope.Equal[CoreOps.GetShortWireName[w1], Rope.FromRefText[t2]],
ENDCASE => ERROR,
r1: ROPE => WITH wr2 SELECT FROM
w2: CoreCreate.Wire => Rope.Equal[r1, CoreOps.GetShortWireName[w2]],
r2: ROPE => Rope.Equal[r1, r2],
t2: REF TEXT => Rope.Equal[r1, Rope.FromRefText[t2]],
ENDCASE => ERROR,
t1: REF TEXT => WITH wr2 SELECT FROM
w2: CoreCreate.Wire => Rope.Equal[Rope.FromRefText[t1], CoreOps.GetShortWireName[w2]],
r2: ROPE => Rope.Equal[Rope.FromRefText[t1], r2],
t2: REF TEXT => Rope.Equal[Rope.FromRefText[t1], Rope.FromRefText[t2]],
ENDCASE => ERROR,
ENDCASE => 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;
};
Core Connection
fsaClass: Core.CellClass ← CoreIO.RegisterClass[
Rosemary.BindCellClass[NEW [Core.CellClassRec ← [name: "FSA", recast: RecastFSA, properties: CoreProperties.Props[[PWCore.layoutAtomProp, $Recast]]]], Rosemary.Register["FSARoseClass", InitFSA, EvalFSA]],
WriteFSA, ReadFSA];
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 = {
[h: Handle, cellType: Core.CellType, wireIDTab: RefTab.Ref, clientData: REF ANYNIL];
WriteExpression: PROC [expr: Boole.Expression] = {
WriteVariable: PROC [out: Core.STREAM, var: Boole.Variable] = {
WITH var SELECT FROM
w: Core.Wire => {
CoreIO.WriteID[h, "w"];
CoreIO.WriteWire[h, wireIDTab, w];
};
s: State => {
CoreIO.WriteID[h, "s"];
CoreIO.WriteAtom[h, s.name];
};
ENDCASE => ERROR;
};
Boole.PutExpr[out: h.stream, expr: expr, putRefAny: WriteVariable];
CoreIO.WriteID[h, NIL];
};
fsa: StateMachine ← NARROW[cellType.data];
count: INT ← 0;
FOR sl: States ← fsa.states, sl.rest UNTIL sl=NIL DO
count ← count + 1;
ENDLOOP;
CoreIO.WriteInt[h, count];
FOR sl: States ← fsa.states, sl.rest UNTIL sl=NIL DO
IF sl.first.name=NIL THEN ERROR;
CoreIO.WriteAtom[h, 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;
CoreIO.WriteInt[h, count];
FOR tl: Transitions ← sl.first.transitions, tl.rest UNTIL tl=NIL DO
WriteExpression[tl.first.expr];
CoreIO.WriteAtom[h, tl.first.target.name];
ENDLOOP;
ENDLOOP;
count ← 0;
FOR ol: Outputs ← fsa.outputs, ol.rest UNTIL ol=NIL DO
count ← count + 1;
ENDLOOP;
CoreIO.WriteInt[h, count];
FOR ol: Outputs ← fsa.outputs, ol.rest UNTIL ol=NIL DO
CoreIO.WriteWire[h, wireIDTab, ol.first.output];
WriteExpression[ol.first.expr];
ENDLOOP;
CoreIO.WriteAtom[h, fsa.initialState.name];
};
ReadFSA: CoreIO.ClassReadProc = {
[h: Handle, cellType: Core.CellType, wireIDTab: RefTab.Ref, clientData: REF ANYNIL];
ReadExpression: PROC RETURNS [expr: Boole.Expression] = {
ReadVariable: PROC [in: Core.STREAM] RETURNS [var: Boole.Variable] = {
type: ROPE ← CoreIO.ReadID[h];
var ← SELECT TRUE FROM
Rope.Equal["w", type] => CoreIO.ReadWire[h, wireIDTab],
Rope.Equal["s", type] => FindState[fsa, CoreIO.ReadAtom[h]],
ENDCASE => ERROR;
};
expr ← Boole.GetExpr[in: h.stream, getRefAny: ReadVariable];
};
fsa: StateMachine;
count: INT ← CoreIO.ReadInt[h];
states: LIST OF ATOMNIL;
FOR sc: INT IN [0..count) DO
states ← CONS[CoreIO.ReadAtom[h], states];
ENDLOOP;
fsa ← NewMachine[states];
FOR sl: States ← fsa.states, sl.rest UNTIL sl=NIL DO
count: INT ← CoreIO.ReadInt[h];
FOR tc: INT IN [0..count) DO
expr: Boole.Expression ← ReadExpression[];
target: ATOM ← CoreIO.ReadAtom[h];
NewTransition[fsa, sl.first.name, target, expr];
ENDLOOP;
ENDLOOP;
count ← CoreIO.ReadInt[h];
FOR oc: INT IN [0..count) DO
wire: Core.Wire ← CoreIO.ReadWire[h, wireIDTab];
expr: Boole.Expression ← ReadExpression[];
fsa.outputs ← CONS[[wire, expr], fsa.outputs];
ENDLOOP;
fsa.initialState ← FindState[fsa, CoreIO.ReadAtom[h]];
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: ROPENIL, props: Core.Properties ← NIL, completeCheck: BOOLFALSE, 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.STREAMIO.ROS[];
Boole.PutExpr[out: out, expr: expr, putRefAny: PrintVar];
RETURN [IO.RopeFromROS[out]];
};
END.