Verification of KPN Level Transformations

A verification framework for checking correctness of Kahn process network (KPN) level transformations is presented for multimedia and signal processing applications. The initial and the transformed KPN behaviors are both modelled as array data dependence graphs (ADDGs) and the verification problem is posed as checking of equivalence between the two ADDGs. The key aspect of our scheme is to model a KPN behaviour as an ADDG. The verification framework is explained with channel merging transformations. Experimental results supporting usability of this scheme are also provided.