Verification method of dataflow algorithms in high-level synthesis

Tsung Hsi Chiang*, Lan-Rong Dung

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

8 Scopus citations


This paper presents a formal verification algorithm using the Petri Net theory to detect design errors for high-level synthesis of dataflow algorithms. Typically, given a dataflow algorithm and a set of architectural constraints, the high-level synthesis performs algorithmic transformation and produces the optimal scheduling. How to verify the correctness of high-level synthesis becomes a key issue before mapping the synthesis results onto a silicon. Many tools exist for RTL (Register Transfer Level) design, but few for high-level synthesis. Instead of applying Boolean algebra, this paper adopts the Petri Net theory to verify the correctness of the synthesis result, because the Petri Net model has the nature of dataflow algorithms. Herein, we propose three approaches to realize the Petri Net based formal verification algorithm and conclude the best one who outperforms the others in terms of processing speed and resource usage.

Original languageAmerican English
Pages (from-to)1256-1270
Number of pages15
JournalJournal of Systems and Software
Issue number8
StatePublished - 1 Aug 2007


  • Dataflow graph
  • Formal verification
  • High-level synthesis
  • Petri Net


Dive into the research topics of 'Verification method of dataflow algorithms in high-level synthesis'. Together they form a unique fingerprint.

Cite this