|
A Formal Specification Model for Hardware/Software Codesign
Abstract:
Embedded controllers for reactive real-time applications are
implemented as mixed software-hardware systems.
In this paper we present a model for
specification, partitioning, and
implementation of such systems.
The model, called Codesign Finite State Machines (CFSMs),
is based on FSMs and is
particularly suited to a specific class of systems with
relatively low algorithmic complexity.
Pre-existing
formal specification languages can be used by the designer to specify the
intended behavior of the system and mapped into our model.
CFSMs use a non-zero unbounded reaction delay model and hence can be
indifferently implemented either in hardware or in software.
The implementation only restricts the range of variation of
some previously undefined delays,
thus preserving formal properties of the
specification across implementation refinements.
The communication primitive, event broadcasting, is low-level enough to
be implemented efficiently and yet general enough to allow higher-level
mechanisms (such as channels) to be defined by the designer.
UCB Design Technology Warehouse Homepage
|
