Translation validation was introduced in the 90's by Pnueli et al. as a technique to formally verify correctness of code generated from the data-flow synchronous language Signal. Rather that certifying the code generator (by writing it entirely using a theorem prover) or exhaustively qualifying it (by obeying to the 27 documentations required as per the DO-178C) translation validation provides a scalable approach to assessing the functional correctness of automatically generated code. By revisiting transition validation, which in the 90's suffered from the limitations of theorem proving and model checking technologies available then, we aim at developing a scalable and flexible approach that can apply to an existing 500k-lines implementation of Signal, Polychrony, and handle large-scale, possibly automatically generated, Signal programs, while using of-the-shelf, efficient, model-checkers and Sat/Smt-solving libraries. We implement translation validation in step-by-step fashion, by proving each transformation of an initial specification separately from the others, until the latest step of actual C-code generation. In this paper, we focus on proving the preservation of timing properties during the compilation process. We use an SMT-solver (Satisfiability Modulo Theory) for checking that the, so-called, implicit \textit{clock model} of a specification as a formula over boolean variables conforms to its implementation. This boolean formula is an important transformation performed by the compiler, as it deterministically characterizes the presence/absence status of all discrete signals manipulated by the specification (inputs and outputs) given that of its trigger.