Full metadata record
DC FieldValueLanguage
dc.contributor.authorLee, Chi-Huien_US
dc.contributor.authorShih, Che-Huaen_US
dc.contributor.authorHuang, Juinn-Daren_US
dc.contributor.authorJou, Jing-Yangen_US
dc.date.accessioned2014-12-08T15:21:18Z-
dc.date.available2014-12-08T15:21:18Z-
dc.date.issued2011en_US
dc.identifier.isbn978-1-4244-7516-2en_US
dc.identifier.urihttp://hdl.handle.net/11536/15117-
dc.description.abstractThis 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.en_US
dc.language.isoen_USen_US
dc.titleEquivalence Checking of Scheduling with Speculative Code Transformations in High-Level Synthesisen_US
dc.typeProceedings Paperen_US
dc.identifier.journal2011 16TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE (ASP-DAC)en_US
dc.contributor.department電子工程學系及電子研究所zh_TW
dc.contributor.departmentDepartment of Electronics Engineering and Institute of Electronicsen_US
dc.identifier.wosnumberWOS:000299427300102-
Appears in Collections:Conferences Paper