標題: VERIFICATION OF DATAFLOW SCHEDULING
作者: Chiang, Tsung-Hsi
Dung, Lan-Rong
電控工程研究所
Institute of Electrical and Control Engineering
關鍵字: Formal verification;high-level synthesis;dataflow;Petri net;model checking
公開日期: 1-Sep-2008
摘要: This paper presents the formal verification method for high-level synthesis (HLS) to detect design errors of dataflow algorithms by using Petri Net (PN) and symbolic-model-verifier (SMV) techniques. Formal verification in high-level design means architecture verification, which is different from functional verification in register transfer level (RTL). Generally, dataflow algorithms need algorithmic transformations to achieve optimal goals and also need design scheduling to allocate process or resources before mapping on a silicon. However, algorithmic transformations and design scheduling are error-prone. In order to detect high-level faults, high-level verification is applied to verify the synthesis results in HLS. Instead of applying Boolean algebra in traditional verification, this paper adopts both Petri Net theory and SMV model checker to verify the correctness of the synthesis results of the high-level dataflow designs. In the proposed hybrid verification method, a high-level designor DUV (design-under-verification) is first transformed into a Petri Net model. Then, Petri Net theory is applied to check the correctness of its algorithmic transformations of HLS, and the SMV model checker is used to verify the correctness of the design scheduling. We presented two approaches to realize the proposed verification method and concluded the best one who outperforms the other in terms of processing speed and resource usage.
URI: http://dx.doi.org/10.1142/S0218194008003891
http://hdl.handle.net/11536/8440
ISSN: 0218-1940
DOI: 10.1142/S0218194008003891
期刊: INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING
Volume: 18
Issue: 6
起始頁: 737
結束頁: 758
Appears in Collections:Articles


Files in This Item:

  1. 000262084900002.pdf