Static scheduling and software synthesis for dataflow graphs with symbolic model-checking

Zonghua Gu; Mingxuan Yuan; Nan Guan; Mingsong Lv; Xiuqiang He; Qingxu Deng; Ge Yu

doi:10.1109/RTSS.2007.51

Static scheduling and software synthesis for dataflow graphs with symbolic model-checking

Zonghua Gu, Mingxuan Yuan, Nan Guan, Mingsong Lv, Xiuqiang He, Qingxu Deng, Ge Yu

Research output: Chapter in book / Conference proceeding › Conference article published in proceeding or book › Academic research › peer-review

11 Citations (Scopus)

Abstract

In this paper, we address the problem of static scheduling and software synthesis for dataflow graphs with the symbolic model-checker NuSMV using a two-step process: first use model-checking to obtain a static schedule with the objective of minimizing the data buffer size, then synthesize efficient code from the static schedule with the objective of minimizing code size and performance overheads due to runtime dynamic decisions. We show the effectiveness of these techniques using a number of digital signal processing examples.

Original language	English
Title of host publication	Proceedings - 28th IEEE International Real-Time Systems Symposium, RTSS 2007
Pages	353-364
Number of pages	12
DOIs	https://doi.org/10.1109/RTSS.2007.51
Publication status	Published - 1 Dec 2007
Externally published	Yes
Event	28th IEEE International Real-Time Systems Symposium, RTSS 2007 - Tucson, AZ, United States Duration: 3 Dec 2007 → 6 Dec 2007

Conference

Conference	28th IEEE International Real-Time Systems Symposium, RTSS 2007
Country/Territory	United States
City	Tucson, AZ
Period	3/12/07 → 6/12/07

ASJC Scopus subject areas

Software
Hardware and Architecture
Computer Networks and Communications

More information

10.1109/RTSS.2007.51

Cite this

@inproceedings{c5bf2158bf9d4404bc1341af475d30bf,

title = "Static scheduling and software synthesis for dataflow graphs with symbolic model-checking",

abstract = "In this paper, we address the problem of static scheduling and software synthesis for dataflow graphs with the symbolic model-checker NuSMV using a two-step process: first use model-checking to obtain a static schedule with the objective of minimizing the data buffer size, then synthesize efficient code from the static schedule with the objective of minimizing code size and performance overheads due to runtime dynamic decisions. We show the effectiveness of these techniques using a number of digital signal processing examples.",

author = "Zonghua Gu and Mingxuan Yuan and Nan Guan and Mingsong Lv and Xiuqiang He and Qingxu Deng and Ge Yu",

year = "2007",

month = dec,

day = "1",

doi = "10.1109/RTSS.2007.51",

language = "English",

isbn = "0769530621",

pages = "353--364",

booktitle = "Proceedings - 28th IEEE International Real-Time Systems Symposium, RTSS 2007",

note = "28th IEEE International Real-Time Systems Symposium, RTSS 2007 ; Conference date: 03-12-2007 Through 06-12-2007",

}

Gu, Z, Yuan, M, Guan, N, Lv, M, He, X, Deng, Q & Yu, G 2007, Static scheduling and software synthesis for dataflow graphs with symbolic model-checking. in Proceedings - 28th IEEE International Real-Time Systems Symposium, RTSS 2007., 4408319, pp. 353-364, 28th IEEE International Real-Time Systems Symposium, RTSS 2007, Tucson, AZ, United States, 3/12/07. https://doi.org/10.1109/RTSS.2007.51

Static scheduling and software synthesis for dataflow graphs with symbolic model-checking. / Gu, Zonghua; Yuan, Mingxuan; Guan, Nan et al.
Proceedings - 28th IEEE International Real-Time Systems Symposium, RTSS 2007. 2007. p. 353-364 4408319.

Research output: Chapter in book / Conference proceeding › Conference article published in proceeding or book › Academic research › peer-review

TY - GEN

T1 - Static scheduling and software synthesis for dataflow graphs with symbolic model-checking

AU - Gu, Zonghua

AU - Yuan, Mingxuan

AU - Guan, Nan

AU - Lv, Mingsong

AU - He, Xiuqiang

AU - Deng, Qingxu

AU - Yu, Ge

PY - 2007/12/1

Y1 - 2007/12/1

N2 - In this paper, we address the problem of static scheduling and software synthesis for dataflow graphs with the symbolic model-checker NuSMV using a two-step process: first use model-checking to obtain a static schedule with the objective of minimizing the data buffer size, then synthesize efficient code from the static schedule with the objective of minimizing code size and performance overheads due to runtime dynamic decisions. We show the effectiveness of these techniques using a number of digital signal processing examples.

AB - In this paper, we address the problem of static scheduling and software synthesis for dataflow graphs with the symbolic model-checker NuSMV using a two-step process: first use model-checking to obtain a static schedule with the objective of minimizing the data buffer size, then synthesize efficient code from the static schedule with the objective of minimizing code size and performance overheads due to runtime dynamic decisions. We show the effectiveness of these techniques using a number of digital signal processing examples.

UR - http://www.scopus.com/inward/record.url?scp=48649086154&partnerID=8YFLogxK

U2 - 10.1109/RTSS.2007.51

DO - 10.1109/RTSS.2007.51

M3 - Conference article published in proceeding or book

SN - 0769530621

SN - 9780769530628

SP - 353

EP - 364

BT - Proceedings - 28th IEEE International Real-Time Systems Symposium, RTSS 2007

T2 - 28th IEEE International Real-Time Systems Symposium, RTSS 2007

Y2 - 3 December 2007 through 6 December 2007

ER -

Static scheduling and software synthesis for dataflow graphs with symbolic model-checking

Abstract

Conference

ASJC Scopus subject areas

More information

Other files and links

Fingerprint

Cite this