A Formal Verification Method of Scheduling in High-level Synthesis

2006 ◽  
Author(s):  
C. Karfa ◽  
C. Mandal ◽  
D. Sarkar ◽  
S.R. Pentakota ◽  
C. Reade
Keyword(s):  
Formal Verification ◽  
High Level Synthesis ◽  
Verification Method ◽  
High Level

VERIFICATION OF DATAFLOW SCHEDULING

2008 ◽  
Vol 18 (06) ◽  
pp. 737-758
Author(s):  
TSUNG-HSI CHIANG ◽  
LAN-RONG DUNG
Keyword(s):  
Formal Verification ◽  
Petri Net ◽  
Register Transfer Level ◽  
Functional Verification ◽  
Model Checker ◽  
Symbolic Model ◽  
Verification Method ◽  
Level Design ◽  
High Level ◽  
Design Scheduling

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 processor 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 design or 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.

Verification method of dataflow algorithms in high-level synthesis

2007 ◽  
Vol 80 (8) ◽  
pp. 1256-1270 ◽  
Author(s):  
Tsung-Hsi Chiang ◽  
Lan-Rong Dung
Keyword(s):  
High Level Synthesis ◽  
Verification Method ◽  
High Level

Floorplan-Aware High-Level Synthesis for Generalized Distributed-Register Architectures

2009 ◽  
Vol E92-A (12) ◽  
pp. 3169-3179 ◽  
Author(s):  
Akira OHCHI ◽  
Nozomu TOGAWA ◽  
Masao YANAGISAWA ◽  
Tatsuo OHTSUKI
Keyword(s):  
High Level Synthesis ◽  
High Level
Sign in / Sign up

Export Citation Format

Share Document