  Hierarchical block diagrams (HBDs) are at the heart of embedded system design
tools, including Simulink. Numerous translations exist from HBDs into languages
with formal semantics, amenable to formal verification. However, none of these
translations has been proven correct, to our knowledge. We present in this
paper the first mechanically proven HBD translation algorithm. The algorithm
translates HBDs into an algebra of terms with three basic composition
operations (serial, parallel, and feedback). In order to capture various
translation strategies resulting in different terms achieving different
tradeoffs, the algorithm is nondeterministic. Despite this, we prove its
semantic determinacy: for every input HBD, all possible terms that can be
generated by the algorithm are semantically equivalent. We apply this result to
show how three Simulink translation strategies introduced previously can be
formalized as determinizations of the algorithm, and derive that these
strategies yield semantically equivalent results (a question left open in
previous work). All results are formalized and proved in the Isabelle
theorem-prover.
