A Verified Hardware Synthesis for Esterel Programs

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 trans-lations, and it does not suffer from the schizophre-nia problems of parallel statements. Furthermore, we have proved the correctness of our translation with HOL, so that HOL can be used for formal synthesis.