A Formal Specification Model for Hardware/Software Codesign

Embedded controllers for reactive real-time applications are implemented as mixed softwarehardware 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 mechanism..