Hardware/software synthesis of formal specifications in codesign of embedded systems

CoDesign aims to integrate the design techniques of hardware and software. In this work, we present a CoDesign methodology based on a formal approach to embedded system specification. This methodology uses the Templated T-LOTOS language to specify the system during all design phases. Templated T-LOTOS is a formal language based on CCS and CSP models. Using Templated T-LOTOS, a system can be specified by observing the temporal ordering in which the events occur from the outside. In this paper we focus on the synthesis of system specified by Templated T-LOTOS. The proposed synthesis algorithm takes advantage of peculiarities of Templates T-LOTOS. Hardware modules are translated into a register transfer-level language that manages some signals in order to drive synchronization, while the software modules are translated into C according to a finite state model whose operations are controlled by a scheduler. The synthesis of the Templated T-LOTOS specification is based on the direct translation of the language operators to ensure that the implemented system is the same as the specified one.