Abstract
In this poster, we present a new specification technique for complex hardware-software systems, based on standard high-level programming languages, such as C, C++, Java, Scheme, or Ada, without extensions or semantic changes. Unlike previous approaches, the designer may choose the model of computation (MoC) and the specification language that best suits her needs, while still being able to formally verify the correctness of the specification. The details of the available hardware and software resources, and the implementation of the different models of computation are encapsulated in libraries to maximize reuse in system specifications.The main benefits obtained from our approach can be summarized as follows: The designer is free to choose the system specification language and the underlying model of computation, independently of the final implementation (software or hardware) of the components. New specification languages and MoCs can be added easily. Simulation of the whole system is straightforward and available tools for formal verification can be used for the different models of computation implemented in our libMoC library. Hardware components can be efficiently synthesized for the part of the system that uses libMoC.