A compositional model for the functional verification of high-levelsynthesis results

摘要

High-level synthesis systems, such as Amical, translate anbehavioral description to an abstract automaton in which the states arendecision and synchronization points, and operations are executed on thenstate transitions. After the scheduling and allocation of the functionalnunits, the system is modeled as the interconnection of an operative andna control part. To formally verify this synthesis mechanism, we combinena detailed state encoding of the control part with an abstract view ofnthe data part. We only compute the set of reachable states of thencontrol part, and compose functional expressions in the data part. Wenshow that, for each of two corresponding state transitions in thenabstract automaton and in the synthesized control part, the expressionsncomputed in the data registers and outputs are equal