Esterel EDA

How can I be sure that generated RTL and generated C have the same behavior?

The behavior is guaranteed by construction, due to the fact that the Esterel language has a formal semantic and thanks to the implemented single compilation flow.