VHDL Code Generation from Formal Event-B Models

In this paper, we present an approach that allows to generate VHDL code from formal models developed with the Event-B formalism. The approach is based on the relationship between the structure of the formal model and hardware description language statements. We are aiming at getting VHDL code whose behaviour is the same as the behaviour of the Event-B model. Our contribution lies in the fact that we show the main similarity between the formal model and VHDL code that allows us to derive the method and, hence, the algorithm for automatic translation. This algorithm can be implemented as a plug-in for the Rodin tool which supports the Event-B formalism. The approach is presented through a simplified version of an industrial case study developed in a stepwise refinement manner. We also present several ways of possible translation depending on the way the model has been developed through refinement. In addition, we present synthesis results that show space occupied by the VHDL code generated.