A symbolic methodology for formal verification of high-level data-flow synthesis

This paper presents a new symbolic methodology for the formal verification of high-level data-flow synthesis process. In the approach, high-level specification of a data-flow design is modeled with Kleene algebra with tests (KAT) as a relational expression. By analyzing this relational expression, assertions that establish properties of the high-level specification are obtained. Then, the problem of high-level data-flow synthesis verification is reduced to the task of checking whether the architectural implementation generated by the synthesis procedure satisfies these asserted properties. A Wu¿s method based property checking approach is integrated into the verification framework to solve this problem. The experimental results on some benchmark and practical designs demonstrate the efficiency of the approach.