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;
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, 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]];
};