We present timed dependence flow graphs, an intermediate form for high-level synthesis from specifications
written in behavioral hardware description languages. Timed dependence flow graphs express data,
control, resource access, and timing dependences, and can be constructed in linear time from behavioral
VHDL descriptions. We also present a formal execution semantics for timed dependence flow graphs,
which we are using in verification of our high-level synthesis tools.