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

High-level synthesis systems, such as Amical, translate a behavioral description to an abstract automaton in which the states are decision and synchronization points, and operations are executed on the state transitions. After the scheduling and allocation of the functional units, the system is modeled as the interconnection of an operative and a control part. To formally verify this synthesis mechanism, we combine a detailed state encoding of the 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 expressions in the data part. We show that, for each of two corresponding state transitions in the abstract automaton and in the synthesized control part, the expressions computed in the data registers and outputs are equal.