Suzan Szollar and A. Richard Newton Introduction

The Evolution of Formal Models for High Level Synthesis and the Introduction of Mealy Machines as a Model for System Behavior

Suzan Szollar and A. Richard Newton

1. Introduction

In the past, functionally described systems were simulated in order to validate their anticipated behavior. More recently, formal verification has been applied because of the advantages of having more than one approach to checking a design. Formal verification is based on applying proven mathematical principles to a behavioral description to determine its validity. It can be applied at the early stages of the design, increasing the overall speed of the design cycle. Because of the advantages of proving the properties of a system mathematically along with simulation, it has become important for the models used to describe system behavior to be verifiable. For this reason, models must be formally defined, and the semantics of finite-automata provides a common mathematical language.

The finite automaton is a mathematical model of a system, with discrete inputs and outputs [8]. The system can be in any one of a finite number of states. The state of the system summarizes the information concerning past inputs needed to determine the behavior of the system on subsequent inputs.

A finite automaton (FA) consists of a finite set of states and a set of transitions from state to state that occur on input symbols chosen from an alphabet . For each input symbol there is exactly one transition out of each state (possibly back to the state itself). Formally, a finite automaton is a 5-tuple (Q, , , q₀, F), where Q is a finite set of states,  is a finite input alphabet, q₀ in Q is the initial state, F  Q is the set of final states, and  is the transition function mapping Q x  to Q. That is,  (q, a) is a state for each state q and input symbol a [8].

A nondeterministic finite automaton (NFA) allows zero, one or more transitions from a state on the same input symbol. Formally the NFA is defined the same as the FA with the exception that  is a map from Q x  to 2^Q (which is the power set of Q, the set of all subsets of Q).

In the next section, the evolution of models leading toward robust and verifiable forms is surveyed, along with the shift in creating models for hardware implementations to the incorporation of both hardware and software considerations. Finite-state Machines are introduced as the preliminary model, completely verifiable but not powerful enough to describe complex systems. Next, Finite-state Machines with Datapaths (FSMD) are shown to provide the means for specifying large systems, however the communication between FSMDs is not explicitly defined. Thus the Behavioral Finite State Machine (BFSM) is studied, because communication is specified, as the partial ordering of events. The BFSM falls short of an ideal model because, while its properties can be proven through simulation, it’s not clear that the BFSM can be formally verified. For this reason, the Co-design Finite-state Machine is introduced, which incorporates both the advantages of the FSMD as well as a rigorous definition of communication between CFSMs, but doesn’t clearly and formally satisfy questions of composition. For this reason, we introduce Communicating Mealy Machines (CMM) and explore why they provide a better model for system behavior, examining both the potential drawbacks and the advantages.

2. 
   Models
   

Synthesis is generally done from internal representations of high-level behavioral descriptions. These internal representations are more general models themselves, while the behavioral models to be examined can be thought of as a subset which satisfy given constraints on their behavior. One of the initial formalisms for showing data dependency relationships was the Data Flow Graph (DFG) [5]. The DFG however, is not sufficient for representing control flow, branching, loops, and procedure calls. For this reason, the Value Trace (VT) was proposed by Snow [12], which, like the DFG, is a directed acyclic graph but additionally the control constructs are preserved and translated into their data flow equivalents (ISP is the HDL used for behavioral descriptions which are ultimately internally represented as VTs). One implementation of the VT is to add control and sequencing information to the VT itself [9]. While this complicates the structure, it alleviates problems caused by having to keep parallel structures or rebuilding information later for identification and verification purposes, and to make partitioning and allocation tractable. There are five types of information represented in the VT: data flow, control flow, resource usage, context, identification and qualifiers[9]. Similarly, the Control Data Flow Graph (CDFG) is an augmented DFG which allows representation of control constructs such as branches and loops. Data dependency is represented within separate basic-blocks which hold the assignment statements of the original behavioral description. One disadvantage of using CDFGs for synthesis directly is that two sequential basic-blocks can never execute together even if they have no data dependencies, because of the requirement that the block structure be maintained. Synthesis is made more efficient by the removal of user-defined control constructs and the introduction of an execution order based on data dependencies. These ideas are incorporated in the VT and ADD representations [5].

A finite state machine (FSM) [6] can be an abstraction of a synchronous circuit [10]. Sequential synthesis is based on the FSM model. Associated with an FSM are a set of input and output values, a set of states and initial states, and a set of transitions. Formally, a synchronous FSM is a six-tuple:

M = {Q, , , , , q₀}

Q is a finite set of states,  is the finite input alphabet,  is the finite output alphabet,  is the transition function mapping Q x  to Q,  is the output function mapping Q x  to , and q₀ is the initial state in Q.

Networks of communicating FSMs can be used to model the behavior of control dominated systems (e.g. ASICs). The advantages of using the FSM network model are given to be the following:

• 
  The model supports behavioral and structural optimization.
  
• 
  Compilation algorithms can blur the distinction between data and control.
  
• 
  Algorithms can be designed to use the FSM network as both input and output.
  
• 
  Because the model is based on Boolean algebra and automata theory, it has well-defined notions of composition, decomposition, and minimality of representation. It also has a lot of flexibility in repartitioning the behavior description, which can expose new optimizations.
  
• 
  Implementation costs, particularly the cost of control, can be measured accurately because the model can be directly implemented as layout.
  

Therefore, for control dominated architectures, FSMs provide an effective behavioral representation which is flexible enough to be manipulated for optimization purposes [17].

The FSM with Datapath (FSMD) [5, 6], otherwise known as the Extended FSM (EFSM), is an adaptation of the FSM to handle complex systems. An FSMD is targeted for both control and data (e.g. FIR filter) dominated systems. It is like the FSM but additionally the transition relation depends on a set of internal variables. Thus, the next state of an FSMD depends on inputs, state, and a signal which ascertains whether a relation between two expressions is true or false. An example of an expression might be: x = (a² + b²)^1/2, and a relation might be: a + b > x - 1.

M = {S, VAR, A, EXP, STAT}

The Behavioral FSM (BFSM) has partially ordered input and output events with respect to time. Scheduling all the inputs and outputs for a BFSM results in a register transfer FSM (RTFSM), whose inputs and outputs are completely determined in time. The BFSM is targeted primarily for synthesis and verification of synchronous hardware systems scheduled statically. Since communication between software components is generally asynchronous, they are scheduled dynamically. Handshaking must be implemented if communication of hardware components are not scheduled statically.

A BFSM has an internal state, and accepts a set of input events and constraints which satisfy one of its defined behaviors in its present state. It then emits a set of constrained output events and changes state [13]. Output events can also be constrained against input events, when an output is desired after a specified number of clock cycles after the input has been consumed. The following properties are given for the BFSM:

• 
  The number of input and output events on any transition is finite.
  
• 
  Both the next-state and output events on any transition is finite.
  
• 
  Both the next-state and output functions are causal, i.e., they depend only on past and present values of the inputs.
  
• 
  In a fully-scheduled RTFSM implementation of a BFSM, any transition takes a finite, constant number of cycles to complete, but different transitions may take different numbers of cycles to complete.
  
• 
  A BFSM is deterministic -- only one transition has its firing condition satisfied at any given time. The model can be extended to include non-deterministic behavior.
  

BFSMs have prototype events and event instances. Event instances are created during execution each time a prototype event is encountered, the instance is indexed to distinguish it from other instances. Timing constraints are expressed between prototype events in the BFSM specification and translated into timing constraints that instances of events must obey. Formally, a BFSM is defined as:

 :  x S  S is the next state function and  : S   is the output function.  and  are input and output event sets. Constraints on the relative times of events are given by C, a set of timing constraints.

The co-design finite state machine (CFSM) [1] is a globally asynchronous, locally synchronous (GALS) model. The CFSM is based on the EFSM model, and each transition in the model is atomic. The execution delay of a CFSM transition is assumed to be non-zero to avoid the composition problems of Mealy machines, (due to feedback loops without delays). Communication between CFSMs is by means of events, semi-synchronized communication primitives. Traditionally, communication of FSMs has been through variables that are shared. Such variables create problems based on the order in which they are accessed and changed. Events are emitted over a set of carriers called signals, and can be detected by one or more CFSMs, where each CFSM has its own copy of the event. The semantics describing the properties of a CFSM are such that each has a finite state machine part, with inputs, outputs, state, a transition relation, and an output relation, and a data computation part with references in the transition relation to external, instantaneous (combinational) functions. A CFSM has locally synchronous behavior, executing a transition by producing a single output reaction based on a single input assignment in zero time. The model also has globally asynchronous behavior, reading inputs, executing a transition, and producing an output in an unbounded but finite amount of time. Formally, a CFSM is defined as:

C

FSM networks assume a single sender and at least one receiver. The communication mechanism is multicast because of the one place buffer between CFSMs, a sender emits an event and each receiver has a private copy of it. A network is a set of CFSMs and nets composed of a set of software CFSMs, hardware CFSMs, and the interfaces between them (e.g., a polling or interrupt scheme to pass events). CFSMs have both Moore and Mealy machine-like properties, although strictly they are neither. CFSMs can self-trigger, thus an output of a machine can be its input. This condition is allowed for efficiency and to make composition of CFSMs possible. Because of the buffer between CFSMs, the machines seem to be Moore-like, however because the delay in the buffer is unspecified, meaning that it can be shorter or longer than a clock cycle, they are not actually Moore machines. Once the machines are composed (Figure 1.), the latches can be removed and the behavior is Mealy-like. At the specification level, the delays aren't necessarily additive when the machines are composed, the only requirement is that there are no combinational loops, and thus there is  (greater than zero) amount of delay. This model is defined such that it is guaranteed that the composition of two CFSMs results in another CFSM.

Figure 1.
A global scheduler controls the interaction of the CFSMs. Each CFSM can be idle or executing, which is when it reads inputs, performs a computation, and possibly changes state and writes its outputs. For each execution, each input signal is read once, each input event is cleared at every execution, and there is a partial order on the reading and writing of signals. The model dictates that the event is read before the data because the value has meaning only when a signal is present. For outputs, the data is written before the event, so that it is valid when the event is cast. In POLIS, input events are read atomically to avoid problems that arise from event-data separation.
The current implementation of the model has the following restrictions for efficiency and synthesizability: there must be a unique reset value for each state variable; the transition relation must contain a single initial transition; the transition relation must be deterministic (for a given input assignment and previous state, there may be at most one matching transition); and both for hardware and software, all events are consumed at every transition, including empty execution.
There is a precise language to CFSMs, such that they can be compiled into FSMs and the behavior can be proved by using the semantics of finite automata.
2.5 CMM

Communicating Mealy machines (CMM) are proposed as an alternative model to those just described, yet adopting the properties which prove to be advantageous. As motivation, Table 2 identifies the properties of the models. The Mealy machine model is targeted for both hardware and software implementations, since design of embedded systems must account for both, as well as the communication and partitioning between them. Formally, a Mealy machine is a six-tuple:

Table 2.

Model	Description	Communication	Design Analysis	Internal Representation	Typical Description Language	Target Implementation
FSM	M = {I, O, S, R, T}	Events, partially ordered	Verification Simulation	Naïve intermediate implementation	VHDL	Control Dominated HW
FSMD/ EFSM	M = {S, VAR, A, EXP, STAT}	Handshaking	Simulation	CDFG (control data flow graph)	VHDL	Control and Data Dominated HW
BFSM/ RTFSM	M = {I, O, S, , , , , C, S0 }	Events, partially ordered/scheduled	Simulation	BSTG (behavior state transition graph)	VHDL subset	Both HW & SW
CFSM	M = {S, I, T}	Events, partially ordered, through one place buffer	Verification Simulation	SHIFT: SGRAPH MDD(sw), BLIF(hw)	Esterel	Both HW & SW
CMM	M = {I, O, S, , , q0}	Events, partially ordered	Verification Simulation	CDFG/Value Trace	Java	Both HW & SW

2.5.1 Communication

Communication between Mealy machines can be specified with three degrees of constraints. In the time-independent model, there is no knowledge about the generation of output signals with respect to the input, and therefore the output may be non-deterministic. In situations where there can be little predictability about the delays of a system, the handshaking protocol can be used, sacrificing some speed and efficiency. Where there is more information about when events occur with respect to each other, a partial ordering of events can be specified. A partial order can be specified in several ways, such as an estimate of the time lapse between two computations, an estimate of the minimum/maximum delay constraints needed between initiation of the execution of two operations, or a distribution model indicating the most likely relative time lapse between the computations at its peak. The clocked, or time-absolute model requires that the time at which the events occur, as well as their duration, be mapped directly onto a timeline, making its behavior fully determined in time. This can occur when the time-relative model is assigned a point of origin and the relative units are assigned a time in seconds.

In synchronous reactive systems, which are ideal for designing embedded applications, both self-loops (as described in the CFSM section) and feedback are permitted. The CFSM model maintains determinacy by defining an unspecified delay between each machine. In the case CMMs, the presence of zero-delay feedback loops can cause the system to be non-deterministic, as well as raise issues about ordering and paradoxes in the system. Ordering problems are generally treated by leaving it to a scheduler to handle the sequence in which the blocks of a system are evaluated. One solution to paradoxes is to allow "undefined" to be one of the possible values for channels in a situation where different blocks might want conflicting values on the channels, and restricting the class of functions the block may compute [6]. Non-determinacy is handled by Edwards by requiring the blocks, in this case CMMs, to be monotonic, to guarantee the least solution is unique, and then choosing the least-defined solution. Edwards defines monotonicity as a block which will not change its mind about a result. It will always produce a consistent output for a given defined input. He makes the point that many imperative languages such as C and C++, and here we add Java, implicitly compute such functions, thus importing blocks from these languages is straightforward. His execution procedure deals with feedback loops by using the recursive divide-and-conquer strategy, systematically breaking feedback loops and iterating them to convergence, which he proves to be optimal.

We've reviewed several models proposed for high-level behavioral descriptions, and examined their development to meet the demands of increasingly complex designs. Each stage of the evolution of these models has yielded some advantage and revealed some limitations, and it is our purpose to capitalize on the body of information to propose a model powerful enough to meet the requirements for effective design. While there are necessary compromises in making any selection, we propose that the CMM is a good model for the purpose of designing synchronous-reactive systems, such as embedded systems. While we adopt many of the timing constraints used to order events for BFSMs and CFSMs, we distinguish the CMM model by not insisting on an unspecified delay between each machine, but rather adding an element of delay where it is required, such as in feedback loops. While finding such cases presents challenges, we're more concerned about resolving ambiguities with respect to composition, while maintaining a formal definition of communication between Mealy machines.

Thanks to Harry Hsieh, Marco Sgroi, Tom Shiple, and Stephen Edwards for the discussions on the properties of the models, and for their tutelage and suggestions.

[1] Balarin, Felice, Sentovich, Ellen, Chiodo, Massimiliano, Giusto, Paolo, Hsieh, Harry, Tabbara, Bassam, Sangiovanni-Vincentelli, Alberto, Jurecska, Attila, Lavagno, Luciano, Passerone, Claudio, Suzuki, Kei. Hardware-Software Co-design of Embedded Systems. 1997.