[Pixel]<DATools7.0>Boole>FiniteStateAutomata.mesa!1

FiniteStateAutomata.mesa

Barth, October 31, 1986 5:59:38 pm PST

DIRECTORY Boole, Core;

FiniteStateAutomata: CEDAR DEFINITIONS

IMPORTS Boole = BEGIN

Theory

This interface provides a mechanism for describing finite state automatons. FSAs are circuits with inputs, outputs and a state vector. They are often represented as directed, possibly cyclic, graphs where the nodes represent the states and the arcs represent state transitions.

Both Mealy (outputs are only functions of the state) and Moore (outputs are functions of both the state and the inputs) machines can be described with this interface. If a Moore machine is described then the outputs are a function of the inputs and next state just before the clock edge occurs, i.e. the current output depends on the next state and inputs rather than the present state and inputs. This allows the implementation to use outputs to encode the state if it wishes. The interface allows multiple arcs from one state to another with different output functions.

The representation of the state is purposely hidden from the client. Clients which need to constrain the representation of the state should contact the implementor. A variable of a transition expression should be a member of the public wire of the cell. A variable of an output expression may be a public wire or a state of the state machine. The public of the cell must have wires named "Vdd", "Gnd", "Reset", and "Clock". The machine makes one transition when a positive edge occurs on Clock. When Reset is asserted during a positive clock edge the state machine is forced to the initial state. The output expressions are evaluated at the same time that the transition expressions are evaluated. Inputs wires are used in the transition and output expressions. Output wires should only be used in the output field of an OutputRec.

Some sanity checks are performed when the cell type is created. Transition expresssion variables must refer to publics of the celltype. Output expression variables must refer to public wires or states in the associated state machine. Outputs must be members of public. All states must be source states. All states must be target states except for the initial state. No check is made to ensure that the transition graph is not partitioned. If more than one transition expression becomes true during evaluation then the machine state will become unknown.

Rosemary behavioural procedures are attached to the generated cell type. The cell type has a recast procedure which implements the state machine using Alps.

Types

ROPE: TYPE = Core.ROPE;

Expression: TYPE = Boole.Expression;

StateMachine: TYPE = REF StateMachineRec;

StateMachineRec: TYPE = RECORD [

states: States ← NIL,

outputs: Outputs ← NIL,

initialState: State ← NIL];

States: TYPE = LIST OF State;

State: TYPE = REF StateRec;

StateRec: TYPE = RECORD [

name: ATOM ← NIL,

transitions: Transitions ← NIL];

Transitions: TYPE = LIST OF Transition;

Transition: TYPE = REF TransitionRec;

TransitionRec: TYPE = RECORD [

expr: Expression ← NIL,

target: State ← NIL];

Outputs: TYPE = LIST OF OutputRec;

OutputRec: TYPE = RECORD [

output: Core.Wire,

expr: Expression];

TransitionLiterals: TYPE = LIST OF TransitionLiteral;

TransitionLiteral: TYPE = RECORD [

to: ATOM,

expr: Expression];

Creation

CreateError: SIGNAL [msg: ROPE];

NewMachine: PROC [states: LIST OF ATOM] RETURNS [StateMachine];

NewTransition: PROC [fsa: StateMachine, from, to: ATOM, expr: Expression];

NewTransitions: PROC [fsa: StateMachine, from: ATOM, transitions: TransitionLiterals];

FindState: PROC [fsa: StateMachine, state: ATOM] RETURNS [State];

StateSeq: PROC [states: LIST OF ATOM, root: ROPE, count: NAT] RETURNS [newStates: LIST OF ATOM];

Mealy: PROC [fsa: StateMachine, state: ATOM, outputs: LIST OF Core.Wire, transitions: TransitionLiterals];

Core Connection

StateMachineCell: 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];

Checks that all source states are target states and vice versa. If completeCheck is TRUE then checks that, starting from each state, the possible transitions cover the input space and that no pair of transition is ambiguous, that is the OR of all transition expressions is TRUE and that pairwise AND of any two transition expressions is FALSE. Under the user assertion on inputs, what we need to prove is that assert implies OR of all transition expressions and that assert implies NOT AND of pairwise transition expressions. Id est:

assert -> all <=> (NOT assert) OR all = true

assert -> ~(e1 AND e2) <=> assert AND e1 AND e2 = false

Hence, the check under constraint consists in initializing the global OR to NOT assert and of checking that the global OR is Equal to true and that for each pair (e1,e2), assert AND e1 AND e2 is Equal to false.

END.