System-level veri cation on high-level synthesis of dataflow graph

Abstract

This paper presents a system-level veri cation algorithm,,using the Petri Net theory to detect design errors for high-level synthesis of dataflow graphs. Typically, given a dataflow graph and a set of architectural constraints, the high-level synthesis performs algorithmic transformation and produces the optitrial scheduling. How to verify the correctness of highlevel synthesis becomes a key issue before mapping the synthesis results onto a silicon. Many tools exist for RTL design, but few for high-Revel synthesis. Instead of applying Boolean algebra, this paper adopts the Petri Net theory to verify the correctness of the synthesis result. Herein, we propose three approaches to realize the Petri Net based formal veri cation algorithm and identify the best one that outperforms the others in terms of processing speed and resource usage.