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 Introduction
The proliferation of embedded hardwaresoftware systems, along with the increasing number of transistors per chip, has compelled designers to reevaluate the design process and develop higher levels of abstraction to handle the design of these systems. The methodology that has evolved presents limitations which must be resolved before significant steps can be taken in the development of next generation of design tools. Currently, specification capture is done by describing the system functionality in a chosen language to comply with a chosen model. The intended result is a functional specification free of implementation detail which is validated by simulation and/or verification. Having a purely functional specification makes it possible to detect errors earlier in the design cycle as well as explore different implementations and partitions in the design space before synthesis. One obstacle to realizing this methodology is that of syntactic variance. While behavioral descriptions might be semantically equivalent, synthesis tools provide results which are highly sensitive to description style. There are two approaches to removing this discrepancy, one is to define a set of modeling guidelines for the initial description, which force a unique input form, and the second is to have the synthesis tool transform the constructs into a unique internal format. Another problem is that no single language or model supports all the necessary functionality and features. There has been a continuing struggle between capitalization on the ideal characteristics of a design language and the incorporation of a mathematical model of behavior into these languages. As a result most approaches to creating a design language today consist of creating a subset of some common language (C or VHDL), or creating an entirely new language fundamentally rooted in the model of computation. Table 1., borrowed from Dan Gajski’s paper, [6], illustrates the many languages available. Predecessors in the evolution of these languages include CDL, DDL, AHPL, ISPS, ISP’, and TIHDL, the “strawman” for VHDL [3].
1.1 Formal Verification
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 finiteautomata provides a common mathematical language.
1.2 Finite Automata
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.
1.2.1 Definition of Finite Automata
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 5tuple (Q, , , q_{0}, F), where Q is a finite set of states, is a finite input alphabet, q_{0 }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].
1.2.2 Definition of Nondeterministic Finite Automata
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).
1.3 The Evolution of Models
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. Finitestate Machines are introduced as the preliminary model, completely verifiable but not powerful enough to describe complex systems. Next, Finitestate 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 Codesign Finitestate 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.
Table 1. S: Fully Supported; P: Partially Supported; N: Not Supported; N/A: Not Applicable.
Language

State
Transitions

Behavioral
Hierarchy

Concurrency

Program Constructs

Exceptions

Behavioral
Completion

VHDL

N

P

S

S

N

S

Verilog

N

S

S

S

S

S

HardwareC

N

P

S

S

N

S

CSP

N

S

S

S

N

S

Statecharts

S

S

S

N

S

N

SDL

S

P

S

N

N

S

Silage

N/A

N/A

S

N/A

N/A

N/A

Esterel

N

S

S

S

S

S

SpecCharts

S

S

S

S

S

S


Models
In the following sections the progress of defining models suitable for the description of both hardware and software systems along with the efforts to make verification possible, in addition to simulation, are chronicled, and a new model, Communicating Mealy Machines (CMM) is introduced.
2.0.1 Internal Representations
Synthesis is generally done from internal representations of highlevel 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 basicblocks which hold the assignment statements of the original behavioral description. One disadvantage of using CDFGs for synthesis directly is that two sequential basicblocks 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 userdefined control constructs and the introduction of an execution order based on data dependencies. These ideas are incorporated in the VT and ADD representations [5].
2.1 FSM
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 sixtuple:
M = {Q, , , , , q_{0}}
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_{0} is the initial state in Q.
For Moore machines, the output depends only on the state. For Mealy machines, the output depends on the input and the state. If the output can be expressed as a function, F : (IxS) (SxO), then it is deterministic. Otherwise it is nondeterministic.
2.1.1 Properties of the FSM
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 welldefined 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].
2.2 FSMD
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^{2 }+ b^{2})^{1/2}, and a relation might be: a + b > x  1.
Formally, to define the FSMD, a set of storage variables, VAR, a set of expressions, EXP = {f(x, y, z, …)]  x, y, z, …, VAR}, a set of storage assignments A = {X e  X VAR, e EXP}, and a set of status signals as the logical relation between two expressions from the set EXP, STAT = {Rel(a, b)  a, b EXP} are introduced [6]. An FSMD is the quintuple:
M = {S, VAR, A, EXP, STAT}
The FSMD is targeted to represent both control and data dominated hardware designs. Variables are used to replace thousands of states. The FSMD is generally implemented with a control unit and a datapath. Each state in the model corresponds to a clock cycle in the implementation [3, 4].
The communication between FSMDs is usually through handshaking, which is synchronized read, synchronized write on a queue of fixed size zero [1].
The argument is made [1] that because the composition of EFSMs is described synchronously, the state explosion problem persists because of the implicit instantaneous communication between them. Additionally, for Moore EFSMs, where the outputs are delayed by one cycle, composition is nonresponsive, whereas for Mealy EFSMs, it is argued that because there can be zero delay between inputs and outputs, a noncausal system can occur. Because combinational feedback loops might occur, correctness of composition must be checked casebycase.
2.3 BFSM
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.
2.3.1 Properties of the BFSM
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 nextstate and output events on any transition is finite.

Both the nextstate and output functions are causal, i.e., they depend only on past and present values of the inputs.

In a fullyscheduled 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 nondeterministic 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:
M = {I, O, S, , , , , C, S_{0 }}
I and O are finite nonempty sets denoting input and output ports of the FSM; S is a finite, nonempty set of states. Two functions define the machine's behavior:
: 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 input to a BFSM is a partially ordered set of events, strictly ordered if events occur on the same label or port. Timing constraints are not used in the execution phase, events are consumed in the order they are received. A transition completes when all essential input events in the transition are matched to corresponding input events that are given by the environment. Transitions give a flow of execution and do not necessarily need to consume time. The duration of transitions and relative time of events are given in terms of clock cycles but are not fixed until scheduling is done. Timing constraints provide some notion of the minimum and maximum times between events, but this information is not sufficient to relate the executions of the BFSM components.
Networks of BFSMs can be used to specify behavior. Input events and output events have a duration of one clock cycle. The absence of an input or output event for a given label represents a don't care value. For this reason, it is difficult to specify a BFSM with a reset or an interrupt since it would require the next state function to be persistently sensitive to a given input. BFSMs can be extended to include next state functions which accommodate sensitive inputs but it's assumed that resets and interrupts are added at the RTFSM implementation.
The semantics of BFSMs are defined by simulation. Therefore, it is unclear whether, for example, there exists a unique BFSM that can represent the composition of two RTFSMs.
Finally, for cases where it is desired to keep the last value until the next output event specifies a new value, a buffer is inserted at the output. This leads to examination of the codesign FSM model, which has an implicit buffer at its inputs and outputs.
2.4 CFSM
The codesign 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 nonzero to avoid the composition problems of Mealy machines, (due to feedback loops without delays). Communication between CFSMs is by means of events, semisynchronized 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:
M = {S, I, T}
S is some finite set of states, I is the set of initial or reset states, and a set of transitions T is called the transition relation.
CFSMs are selectively reactive. They communicate through signals, control signals, and data signals. Associated with a signal are an event and data, and the signal is communicated between CFSMs via a oneplace input buffer, which contains one memory element for the event and one for the data. The event can be emitted by a sender CFSM and consumed by the receiver CFSM. It is detected by reading the event buffer and consumed by setting the buffer to zero. Data may be written by a sender CFSM and read by the receiver CFSM. There is also a state signal which is an internal input/output data signal. It may be written and read by its CFSM. A state is a set of values for the state signals. Communication is initiated through events, thus a CFSM cannot react unless an input event is present.
2.4.1 Communication
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 machinelike properties, although strictly they are neither. CFSMs can selftrigger, 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 Moorelike, 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 Mealylike. 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 eventdata 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 sixtuple:
M = {I, O, S, , , q_{0}}
I and O are the input and output sets, S represents the state. maps I x O to S. Thus a Mealy machine is defined such that the outputs depend on the present state and the present value of the inputs. Mealy machine implementations save states when compared to Moore machine implementations.
A clocking element is introduced into the machine to provide an element of state. The outputs can change when the inputs change, independent of the clock, and therefore without refinement the model has zero delay. Allowing for zero delay between inputs and outputs can cause nondeterministic behavior if at least two machines are put in a loop. We make the argument that such loops can be identified, especially within the language we propose to specify system behavior in, Java, and an element of delay can be inserted in the feedback loop. Although this requires that the code be checked casebycase, the alternative of adding an ambiguous buffer between each machine creates an unnecessary delay overhead, and provides only vague solutions to issues of composition.
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, S_{0 }}

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, , , q_{0}}

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 timeindependent model, there is no knowledge about the generation of output signals with respect to the input, and therefore the output may be nondeterministic. 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 timeabsolute 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 timerelative model is assigned a point of origin and the relative units are assigned a time in seconds.
2.5.2 Composition & Decomposition
In synchronous reactive systems, which are ideal for designing embedded applications, both selfloops (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 zerodelay feedback loops can cause the system to be nondeterministic, 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]. Nondeterminacy 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 leastdefined 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 divideandconquer strategy, systematically breaking feedback loops and iterating them to convergence, which he proves to be optimal.
One of the problems with the composition of Mealy machines is that combinational cycles can arise when a single FSM is synthesized within the context of a set of interacting FSMs [10]. Algorithms have been developed by Malik to detect combinational loops during simulation, revealing when combinational circuits with feedback are stateless. For sequential circuits, cycles which are not well behaved for certain inputs are detected, and it is shown that if those inputs never occur, then the system should be considered wellbehaved [10, 11].
Unwanted dependencies often prevent certain subsystems from being encapsulated, making it difficult to develop complex systems. CFSMs reconcile this particular issue of composition by leaving the amount of delay between machines to be ambiguous, and thus arguing that the composition of two CFSMs results in a CFSM. Similarly, decomposition of CFSMs is made possible because of the unspecified amount of delay, but this is a vaguely defined solution for issues regarding composition. Edwards proposes that partial evaluation allows for such encapsulation, by allowing a block to execute with only partial information about its inputs. Although incomplete inputs produce incomplete outputs, this avoids the addition of synchronization which causes these problems. He also uses recursive stronglyconnected component decomposition to successfully reduce a graph to single nodes.
3.0 Conclusions
We've reviewed several models proposed for highlevel 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 synchronousreactive 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.
Acknowledgements
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.
References
[1] Balarin, Felice, Sentovich, Ellen, Chiodo, Massimiliano, Giusto, Paolo, Hsieh, Harry, Tabbara, Bassam, SangiovanniVincentelli, Alberto, Jurecska, Attila, Lavagno, Luciano, Passerone, Claudio, Suzuki, Kei. HardwareSoftware Codesign of Embedded Systems. 1997.
[2]Barbacci, M. R.. Instruction Set Processor Specifications (ISPS): The Notation and its Applications. IEEE Transactions on Computers, Vol. C30, No. 1, pp. 24040, January 1981.
[3]Chu, Yaohan, Dietmeyer, Donald L., Duley, James R., Hill, Fredrick J., Barbacci, Mario R., Rose, Charles W., Ordy, Greg, Johnson, Bill, Roberts, Martin. Three Decades of HDLs. IEEE Design and Test of Computers, pp. 6981, June 1992.
[4] Edwards, Stephen Anthony. The Specification and Execution of Heterogeneous Synchronous Reactive Systems. Ph.D. thesis, Department of Electrical Engineering, UC Berkeley, Spring 1997.
[5] Gajski, Daniel D., Ramachandran, Loganath. Introduction to HighLevel Synthesis. IEEE Design & Test of Computers, pp. 4454, Winter 1994.
[6] Gajski, Daniel D., Vahid, Frank. Specification and Design of Embedded HardwareSoftware Systems. IEEE Design & Test of Computers, pp. 5367, Spring 1995.
[7] Gupta, Rajesh K, De Micheli, Giovanni. HardwareSoftware Cosynthesis for Digital Systems. IEEE Design & Test of Computers, pp. 2941, September 1993.
[8] Hopcroft, J., Ullman, J.. Introduction to Automata Theory, Languages and Computation. AddisonWesley, 1979.
[9] McFarland, S. J.. The Value Trace: A Data Base for Automated Digital Design. Master’s thesis, Department of Electrical Engineering, CarnegieMellon University, April 1978.
[10] Shiple, Thomas Robert. Formal Analysis of Synchronous Circuits. Ph.D. thesis, Department of Electrical Engineering, UC Berkeley, 1996.
[11] Shiple, Thomas R., Berry, Gerard, Touati, Herve. Constructive Analysis of Cyclic Circuits. Proceedings, European Design and Test Conference ED&TC, pp. 328333, 1996.
[12] Snow, Edward A.. Automation of Module Set Independent RegisterTransfer Level Design. Ph.D. thesis, Department of Electrical Engineering, CarnegieMellon University, April 1978.
[13] Takach, Andres, Wolf, Wayne. An Automaton Model for Scheduling Constraints in Synchronous Machines. IEEE Transactions on Computers, Vol. 44, No. 1, January 1995.
[14] Walker, R. A., Thomas, D. E.. Behavioral Level Transformation in the CMUDA System. Proceedings of the 20^{th} DAC, ACM/IEEE Design Automation Conference, pp. 788789, June 1983.
[15] Walker, R., A., Thomas, D. E.. A Model of Design Representation and Synthesis. Proceedings of the 22^{nd} DAC, ACM/IEEE Design Automation Conference, pp. 453459, June 1985.
[16] Watanabe, Yosinori, Brayton, Robert K.. State Minimization of Pseudo NonDeterministic FSM's. Proceedings, the European Design and Test Conference; EDAC, the European Conference on Design Automation; ETC European Test Conference; EUROASIC, IEEE Computer Society Press, 1994.
[17] Wolf, Wayne. The FSM Network Model for Behavioral Synthesis of ControlDominated Machines. Proceedings, 27^{th} ACM/IEEE Design Automation Conference, Paper 41.3, 1990.
01/30/17 Page of Formal Models
