A verified hardware synthesis of Esterel programs

Abstract

Synchronous programming languages like Esterel are becoming more and more popular for the design of multi-threaded reactive systems. We have embedded a variant of the Esterel language in the interactive theorem prover HOL so that we can formally reason about programs of the language and- at a meta level - about the language itself. Based on a separation of the control and data flow of the programs, we have defined a new translation to equation systems. Our new translation is simpler than state-of-the-art translations, and it does not suffer from the schizophrenia problems of parallel statements. Furthermore, we have proved the correctness of our translation with HOL, so that HOL can be used for formal synthesis. © 2001 by Springer Science+Business Media New York.