A Formal Specification Model for Hardware/Software Codesign

M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L. Lavagno and Alberto L. Sangiovanni-Vincentelli

EECS Department
University of California, Berkeley
Technical Report No. UCB/ERL M93/48
June 1993

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1993/ERL-93-48.pdf

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.

BibTeX citation:

@techreport{Chiodo:M93/48,
    Author = {Chiodo, M. and Giusto, P. and Hsieh, H. and Jurecska, A. and Lavagno, L. and Sangiovanni-Vincentelli, Alberto L.},
    Title = {A Formal Specification Model for Hardware/Software Codesign},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {1993},
    Month = {Jun},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1993/2367.html},
    Number = {UCB/ERL M93/48},
    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.}
}

EndNote citation:

%0 Report
%A Chiodo, M.
%A Giusto, P.
%A Hsieh, H.
%A Jurecska, A.
%A Lavagno, L.
%A Sangiovanni-Vincentelli, Alberto L.
%T A Formal Specification Model for Hardware/Software Codesign
%I EECS Department, University of California, Berkeley
%D 1993
%@ UCB/ERL M93/48
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1993/2367.html
%F Chiodo:M93/48