A compositional model for the functional verification of high-level synthesis results

High-level synthesis systems, such as Amical, translate a behavioral descri ption to an abstract automaton in which the states are decision and synchro nization points, and operations are executed on the state transitions. Afte r the scheduling and allocation of the functional units, the system is mode led as the interconnection of an operative and a control part. To formally verify this synthesis mechanism, we combine a detailed state encoding of th e control part with an abstract view of the data part. We only compute the set of reachable states of the control part, and compose functional express ions in the data part. We show that, for each two corresponding state trans itions in the abstract automaton and in the synthesized control part, the e xpressions computed in the data registers and outputs are equal.