A Method for the Generation of HDL Code at the RTL level form a High-Level Formal Specification Language

Apostolos Kountouris (1) , Christophe Wolinski (2)

1 FT R&D - France Télécom Recherche & Développement
2 EP-ATR - Environnement de programmation d'applications temps réel

In this paper a method for generating HDL code from SIGNAL formal specifications, is described. Applying two transformations on the initial specification yields functionally equivalent RTL HDL code. The functional equivalence is formally proven. The methodology allows component re-usability and enables the validation of their integration at the specification level. We anticipate that the principles presented in this paper, will be applied in the framework of a cooperation with Motorola.

Domaines: Systèmes embarqués

Apostolos Kountouris, Christophe Wolinski. A Method for the Generation of HDL Code at the RTL level form a High-Level Formal Specification Language. 40th Midwest Symposium on Circuits and Systems (MWSCAS '97), Aug 1997, Sacramento, CA, United States. pp.1095-1098. ⟨hal-00545554⟩