A4 Vertaisarvioitu artikkeli konferenssijulkaisussa
Generation of Structural VHDL Code with Library Components from Formal Event-B Models
Tekijät: Ostroumov Sergey, Tsiopoulos Leonidas, Sere Kaisa, Plosila Juha
Toimittaja: Silva Jose, Leporati Francesco
Julkaisuvuosi: 2013
Kokoomateoksen nimi: 2013 Euromicro Conference on Digital System Design (DSD)
Aloitussivu: 111
Lopetussivu: 118
Sivujen määrä: 8
ISBN: 978-0-7695-5074-9
DOI: https://doi.org/10.1109/DSD.2013.20
Tiivistelmä
We propose a design approach to integrating correct-by-construction formal modeling with hardware implementations in VHDL. Formal modeling is performed within the Event-B framework that supports the refinement approach, i.e., stepwise unfolding of system properties in a correct-by-construction manner. After an implementable model of a hardware system is derived, we apply an additional refinement step in order to introduce hardware library components in the form of functions. We show the mapping between these functions and corresponding library components such that structural, i.e., component-based, VHDL implementation is derived. The application of functions binds unrestricted data types and substitutes regular operations with function calls. The approach is presented through examples that illustrate the additional refinement step and the code generation. We show the advantages in terms of occupied area (2,5% and 12,5%) and performance (13,7% and 15,4%) of the descriptions that incorporate hardware library components.
We propose a design approach to integrating correct-by-construction formal modeling with hardware implementations in VHDL. Formal modeling is performed within the Event-B framework that supports the refinement approach, i.e., stepwise unfolding of system properties in a correct-by-construction manner. After an implementable model of a hardware system is derived, we apply an additional refinement step in order to introduce hardware library components in the form of functions. We show the mapping between these functions and corresponding library components such that structural, i.e., component-based, VHDL implementation is derived. The application of functions binds unrestricted data types and substitutes regular operations with function calls. The approach is presented through examples that illustrate the additional refinement step and the code generation. We show the advantages in terms of occupied area (2,5% and 12,5%) and performance (13,7% and 15,4%) of the descriptions that incorporate hardware library components.
Turun yliopiston Tutkimustietojärjestelmän portaali