Timed dependence flow graphs, an intermediate form for verified high-level synthesis

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 call 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