The ´Best´ Valid Safe Protocol Converter

In the hardware world, off-the-shelf heterogeneous components called IPs can be reused to build complex embedded systems such as systems-on-chips (SoCs). Converters are required to bridge these components because of differences in their interfaces. In this work, we present a framework to generate a converter, given rigorous specifications of the component IPs. This framework consists of a front-end that builds a verified raw converter, and a back-end that allows selection of the `best´ converter based on predicted performance. We define protocols with uncontrollability, safeness, validity and correctness conditions, and we use temporal logic to specify properties. A model checker is integrated into the framework to verify the properties. The framework has been implemented, and we illustrate the technique by synthesising a converter for a simple pair of protocols. We also apply our model to industry-standard AMBA bus protocols to show industrial applicability.