Name
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.
|
Year | DOI | Venue |
|---|---|---|
2011 | 10.1109/ASPDAC.2011.5722241 | ASP-DAC |
Keywords | Field | DocType |
high-level synthesis,formal method,common subexpression extraction,finite state machine,equivalence checking,existing state-of-the-art equivalence checking,speculative code transformation,finite set,basic block,code transformation,path-based scheduling,merging,automata,electronic system level,algorithm design,algorithm design and analysis,high level synthesis,scheduling,finite state machines,scheduling algorithm | Formal equivalence checking,Algorithm design,Computer science,Scheduling (computing),Automaton,High-level synthesis,Algorithm,Real-time computing,Finite-state machine,Theoretical computer science,Basic block,Formal methods | Conference |
ISSN | ISBN | Citations |
2153-6961 | 978-1-4244-7516-2 | 17 |
PageRank | References | Authors |
0.82 | 22 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chi-Hui Lee | 1 | 17 | 0.82 |
| Che-Hua Shih | 2 | 39 | 3.73 |
| Juinn-Dar Huang | 3 | 270 | 27.42 |
| Jing-Yang Jou | 4 | 681 | 88.55 |