A flexible specification framework for hardware-software codesign

Presents a new specification technique for complex hardware-sofware 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 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