Equivalence checking of scheduling with speculative code transformations in high-level synthesis

Chi Hui Lee; Che Hua Shih; Juinn-Dar Huang; Jing Yang Jou

doi:10.1109/ASPDAC.2011.5722241

Equivalence checking of scheduling with speculative code transformations in high-level synthesis

Chi Hui Lee^*, Che Hua Shih, Juinn-Dar Huang, Jing Yang Jou

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

36 Scopus citations

Abstract

This paper presents a formal method for equivalence checking between the descriptions before and after scheduling in high-level synthesis (HLS). Both descriptions are represented by finite state machine with datapaths (FSMDs) and are then characterized through finite sets of paths. The main target of our proposed method is to verify scheduling employing code transformations - such as speculation and common subexpression extraction (CSE), across basic block (BB) boundaries - which have not been properly addressed in the past. Nevertheless, our method can verify typical BB-based and path-based scheduling as well. The experimental results demonstrate that the proposed method can indeed outperform an existing state-of-the-art equivalence checking algorithm.

Original language	English
Title of host publication	2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011
Pages	497-502
Number of pages	6
DOIs	https://doi.org/10.1109/ASPDAC.2011.5722241
State	Published - 2011
Event	2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011 - Yokohama, Japan Duration: 25 Jan 2011 → 28 Jan 2011

Publication series

Name	Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

Conference

Conference	2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011
Country/Territory	Japan
City	Yokohama
Period	25/01/11 → 28/01/11

Access to Document

10.1109/ASPDAC.2011.5722241

Cite this

Lee, C. H., Shih, C. H., Huang, J.-D., & Jou, J. Y. (2011). Equivalence checking of scheduling with speculative code transformations in high-level synthesis. In 2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011 (pp. 497-502). Article 5722241 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). https://doi.org/10.1109/ASPDAC.2011.5722241

@inproceedings{d2b42ad79a5448acbc11917d8c398216,

title = "Equivalence checking of scheduling with speculative code transformations in high-level synthesis",

abstract = "This paper presents a formal method for equivalence checking between the descriptions before and after scheduling in high-level synthesis (HLS). Both descriptions are represented by finite state machine with datapaths (FSMDs) and are then characterized through finite sets of paths. The main target of our proposed method is to verify scheduling employing code transformations - such as speculation and common subexpression extraction (CSE), across basic block (BB) boundaries - which have not been properly addressed in the past. Nevertheless, our method can verify typical BB-based and path-based scheduling as well. The experimental results demonstrate that the proposed method can indeed outperform an existing state-of-the-art equivalence checking algorithm.",

author = "Lee, {Chi Hui} and Shih, {Che Hua} and Juinn-Dar Huang and Jou, {Jing Yang}",

year = "2011",

doi = "10.1109/ASPDAC.2011.5722241",

language = "English",

isbn = "9781424475155",

series = "Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC",

pages = "497--502",

booktitle = "2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011",

note = "2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011 ; Conference date: 25-01-2011 Through 28-01-2011",

}

Lee, CH, Shih, CH, Huang, J-D & Jou, JY 2011, Equivalence checking of scheduling with speculative code transformations in high-level synthesis. in 2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011., 5722241, Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC, pp. 497-502, 2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011, Yokohama, Japan, 25/01/11. https://doi.org/10.1109/ASPDAC.2011.5722241

Equivalence checking of scheduling with speculative code transformations in high-level synthesis. / Lee, Chi Hui; Shih, Che Hua; Huang, Juinn-Dar et al.
2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011. 2011. p. 497-502 5722241 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Equivalence checking of scheduling with speculative code transformations in high-level synthesis

AU - Lee, Chi Hui

AU - Shih, Che Hua

AU - Huang, Juinn-Dar

AU - Jou, Jing Yang

PY - 2011

Y1 - 2011

N2 - This paper presents a formal method for equivalence checking between the descriptions before and after scheduling in high-level synthesis (HLS). Both descriptions are represented by finite state machine with datapaths (FSMDs) and are then characterized through finite sets of paths. The main target of our proposed method is to verify scheduling employing code transformations - such as speculation and common subexpression extraction (CSE), across basic block (BB) boundaries - which have not been properly addressed in the past. Nevertheless, our method can verify typical BB-based and path-based scheduling as well. The experimental results demonstrate that the proposed method can indeed outperform an existing state-of-the-art equivalence checking algorithm.

AB - This paper presents a formal method for equivalence checking between the descriptions before and after scheduling in high-level synthesis (HLS). Both descriptions are represented by finite state machine with datapaths (FSMDs) and are then characterized through finite sets of paths. The main target of our proposed method is to verify scheduling employing code transformations - such as speculation and common subexpression extraction (CSE), across basic block (BB) boundaries - which have not been properly addressed in the past. Nevertheless, our method can verify typical BB-based and path-based scheduling as well. The experimental results demonstrate that the proposed method can indeed outperform an existing state-of-the-art equivalence checking algorithm.

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

U2 - 10.1109/ASPDAC.2011.5722241

DO - 10.1109/ASPDAC.2011.5722241

M3 - Conference contribution

AN - SCOPUS:79952981328

SN - 9781424475155

T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

SP - 497

EP - 502

BT - 2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011

T2 - 2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011

Y2 - 25 January 2011 through 28 January 2011

ER -

Equivalence checking of scheduling with speculative code transformations in high-level synthesis

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this