Formal Models for Embedded System Design Embedded System Design 2

Abstract

codesign finite-state machines ACFSM is a formal model that allows one to represent embedded systems specifications, involving both control and DF aspects, at a high level of abstraction. It consists of a network of FSMs that communicates asynchronously by means of events (that at the abstract level denote only partial ordering, not time) over lossless signals with FIFO semantics. ACFSMs are a GALS model: the local behavior is synchronous (from its own perspective), because each ACFSM executes a transition by producing an output reaction based on a snapshot set of inputs in zero time the global behavior is asynchronous (as seen by the rest of the system), since each ACFSM detects inputs, executes a transition, and emits outputs in an unbounded but finite amount of time The asynchronous communication among ACFSMs over an unbounded FIFO channel: supports a (possibly very nondeterministic) specification in which the execution delay of each ACFSM is unknown a priori and, therefore, is not biased toward a specific hardware/software implementation decouples the behavior of each ACFSM from the communication with other ACFSMs. The communication can then be designed by refinement independently from the funcEmbedded System Design 8 IEEE Design & Test of Computers tional specification of the ACFSMs, as we will show later. Single ACFSM behavior A single ACFSM describes a finite-state control operating on a DF. It is an extended FSM, in which the extensions add support for data handling and asynchronous communication. An ACFSM transition can be executed when a precondition on the number of present input events and a Boolean expression over the values of those input events are satisfied. During a transition execution, an ACFSM first atomically detects and consumes some of the input events, then performs a computation by emitting output events with the value determined by expressions over detected input events. A key feature of ACFSMs is that transitions, in general, consume multiple events from the same input signal and produce multiple events to the same output signal (multirate transitions). Next, we formally define an ACFSM. An ACFSM is a triple A = (I, O, T): I = {I1, I2, ... IN} is a finite set of inputs. Let i j i indicate the event that at a certain instant occupies the jth position in the FIFO at input Ii. O = {O1, O2, ... OM} is a finite set of outputs. Let o j i indicate the jth event emitted by a transition on output Oi. T ⊆ {(IR, IB, CR, OR, OB)} is the transition relation, where: 1. IR is the input enabling rate, IR = {(I1, ir1), (I2, ir2), ..., (IN, irN) | 1 ≤ n ≤ N, In ∈ I, irn ∈ N (i.e., irn is the number of input events from each input In that are required to trigger the transition). 2. IB is a Boolean-valued expression over the values of the events {i j i}, 1 ≤ i ≤ N, 1 ≤ j ≤ iri that enable the transition. 3. CR is the input consumption rate, CR = {(I1, cr1), (I2, cr2), ..., (IN, crN) | 1 ≤ n ≤ N, In ∈ I, crn ∈ N, crn ≤ irn ≤ crn = I ALL n }, i.e., crn is the number of input events consumed from each input. The number of events that is consumed should be not greater than the number of events that enabled the transition. It is also possible to specify, by saying that crn = I ALL n , that a transition resets a given input, i.e., it consumes all the events in the corresponding signal (that must be at least as many as those enabling the transition). 4. OR is the output production rate, OR = {(O1, or1), (O2, or2), ..., (OM, orM) | 1 ≤ m ≤ M, Om ∈ O, orm ∈ N} (i.e., orn is the number of output events produced on each output On during a transition execution). 5. OB is a set of vectors of expressions that determines the values of the output events, one vector per output with orn > 0 and one element per emitted event {o j i},1 ≤ i ≤ N,1 ≤ j ≤ ori Note that signals that are at the same time input and output, and for which a single event is produced and consumed at each transition, act as implicit state variables of the ACFSM. If several transitions can be executed in a given configuration (events and values) of the input signals, the ACFSM is nondeterministic and can execute any one of the matching transitions. Nondeterminism can be used at the initial stages of a design to model partial specifications, later to be refined into a deterministic ACFSM. ACFSMs differ from DF networks in that there is no blocking read requirement (i.e., ACFSM transitions, unlike firings in DF networks, can be conditioned to the absence of an event over a signal). Hence, ACFSMs are also not continuous in Kahn’s sense6 (the arrival of two events in different orders may change the behavior). Another difference with DF models is that ACFSMs can “flush” an input signal to model exception handling and reaction to disruptive events (e.g., errors and reinitializations). A DF actor cannot do so, since when the input signal has been emptied, the actor is blocked while waiting for the signal, rather than proceeding to execute the recovery action. A difference from most FSM-based models is the possibility to use multirate transitions to represent production and consumption of events over the same signal at different rates (e.g., images produced line by line and consumed pixel by pixel).