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.
codesign embedded system hardware and software synthesis