1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
|
@article{leroy09_formal_verif_realis_compil,
author = {Leroy, Xavier},
title = {Formal Verification of a Realistic Compiler},
journal = {Commun. ACM},
volume = 52,
number = 7,
pages = {107-115},
year = 2009,
doi = {10.1145/1538788.1538814},
address = {New York, NY, USA},
issn = {0001-0782},
issue_date = {July 2009},
month = jul,
numpages = 9,
publisher = {ACM},
}
@inproceedings{lidbury15_many_core_compil_fuzzin,
author = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson,
Alastair F.},
title = {Many-Core Compiler Fuzzing},
booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design
and Implementation},
year = 2015,
pages = {65-76},
doi = {10.1145/2737924.2737986},
address = {New York, NY, USA},
isbn = 9781450334686,
location = {Portland, OR, USA},
numpages = 12,
publisher = {Association for Computing Machinery},
series = {PLDI '15},
}
@article{takach16_high_level_synth,
author = {A. {Takach}},
title = {High-Level Synthesis: Status, Trends, and Future
Directions},
journal = {IEEE Design Test},
volume = {33},
number = {3},
pages = {116-124},
year = {2016},
doi = {10.1109/MDAT.2016.2544850},
url = {https://doi.org/10.1109/MDAT.2016.2544850},
ISSN = {2168-2364},
month = {June},
}
@inproceedings{liu16_effic_high_level_synth_desig,
author = { {Dong Liu} and B. C. {Schafer}},
title = {Efficient and reliable High-Level Synthesis Design Space
Explorer for FPGAs},
booktitle = {2016 26th International Conference on Field Programmable
Logic and Applications (FPL)},
year = 2016,
pages = {1-8},
doi = {10.1109/FPL.2016.7577370},
ISSN = {1946-1488},
month = {Aug},
}
@article{lahti19_are_we_there_yet,
author = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and
T. D. {H{\"a}m{\"a}l{\"a}inen}},
title = {Are We There Yet? a Study on the State of High-Level
Synthesis},
journal = {IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems},
volume = {38},
number = {5},
pages = {898-911},
year = {2019},
doi = {10.1109/TCAD.2018.2834439},
ISSN = {1937-4151},
month = {May},
}
@misc{mentor20_catap_high_level_synth,
author = {Mentor},
title = {Catapult High-Level Synthesis},
url = {https://www.mentor.com/hls-lp/catapult-high-level-synthesis/c-systemc-hls},
urldate = {2020-06-06},
year = 2020,
}
@inproceedings{gupta03_spark,
author = {S. {Gupta} and N. {Dutt} and R. {Gupta} and A. {Nicolau}},
title = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler
transformations},
booktitle = {16th International Conference on VLSI Design, 2003. Proceedings.},
year = 2003,
pages = {461-466},
doi = {10.1109/ICVD.2003.1183177},
url = {https://doi.org/10.1109/ICVD.2003.1183177},
ISSN = {1063-9667},
month = {Jan},
}
@article{chouksey20_verif_sched_condit_behav_high_level_synth,
author = {R. {Chouksey} and C. {Karfa}},
title = {Verification of Scheduling of Conditional Behaviors in
High-Level Synthesis},
journal = {IEEE Transactions on Very Large Scale Integration (VLSI)
Systems},
volume = {},
number = {},
pages = {1-14},
year = {2020},
doi = {10.1109/TVLSI.2020.2978242},
url = {https://doi.org/10.1109/TVLSI.2020.2978242},
ISSN = {1557-9999},
month = {},
}
@inproceedings{pnueli98_trans,
author = "Pnueli, A. and Siegel, M. and Singerman, E.",
title = "Translation validation",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
year = 1998,
pages = "151--166",
address = "Berlin, Heidelberg",
editor = "Steffen, Bernhard",
isbn = "978-3-540-69753-4",
publisher = "Springer",
}
@article{chouksey19_trans_valid_code_motion_trans_invol_loops,
author = {R. {Chouksey} and C. {Karfa} and P. {Bhaduri}},
title = {Translation Validation of Code Motion Transformations
Involving Loops},
journal = {IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems},
volume = 38,
number = 7,
pages = {1378-1382},
year = 2019,
doi = {10.1109/TCAD.2018.2846654},
ISSN = {1937-4151},
month = {July},
}
@article{banerjee14_verif_code_motion_techn_using_value_propag,
author = {K. {Banerjee} and C. {Karfa} and D. {Sarkar} and C. {Mandal}},
title = {Verification of Code Motion Techniques Using Value
Propagation},
journal = {IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems},
volume = 33,
number = 8,
pages = {1180-1193},
year = 2014,
doi = {10.1109/TCAD.2014.2314392},
ISSN = {1937-4151},
month = {Aug}
}
@inproceedings{kim04_autom_fsmd,
author = { {Youngsik Kim} and S. {Kopuri} and N. {Mansouri}},
title = {Automated formal verification of scheduling process using
finite state machines with datapath (FSMD)},
tags = {hls, verification},
booktitle = {International Symposium on Signals, Circuits and
Systems. Proceedings, SCS 2003. (Cat. No.03EX720)},
year = 2004,
pages = {110-115},
doi = {10.1109/ISQED.2004.1283659},
month = {March}
}
@inproceedings{karfa06_formal_verif_method_sched_high_synth,
author = {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and
Reade, Chris},
title = {A Formal Verification Method of Scheduling in High-level
Synthesis},
tags = {hls},
booktitle = {Proceedings of the 7th International Symposium on Quality
Electronic Design},
year = 2006,
pages = {71--78},
doi = {10.1109/ISQED.2006.10},
acmid = 1126731,
address = {Washington, DC, USA},
isbn = {0-7695-2523-7},
numpages = 8,
publisher = {IEEE Computer Society},
series = {ISQED '06},
}
@inproceedings{leroy06_formal_certif_compil_back_end,
author = {Leroy, Xavier},
title = {Formal Certification of a Compiler Back-End or: Programming
a Compiler with a Proof Assistant},
booktitle = {Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages},
year = 2006,
pages = {42-54},
doi = {10.1145/1111037.1111042},
url = {https://doi.org/10.1145/1111037.1111042},
address = {New York, NY, USA},
isbn = 1595930272,
keywords = {the Coq theorem prover, certified compilation, compiler
transformations and optimizations, program proof, semantic
preservation},
location = {Charleston, South Carolina, USA},
numpages = 13,
publisher = {Association for Computing Machinery},
series = {POPL '06}
}
@book{bertot04_inter_theor_provin_progr_devel,
author = {Yves Bertot and Pierre Cast{\'{e}}ran},
title = {Interactive Theorem Proving and Program Development},
year = 2004,
publisher = {Springer Berlin Heidelberg},
url = {https://doi.org/10.1007/978-3-662-07964-5},
doi = {10.1007/978-3-662-07964-5},
}
@inproceedings{tristan08_formal_verif_trans_valid,
author = {Tristan, Jean-Baptiste and Leroy, Xavier},
title = {Formal Verification of Translation Validators: A Case Study on
Instruction Scheduling Optimizations},
booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages},
year = 2008,
pages = {17-27},
doi = {10.1145/1328438.1328444},
address = {New York, NY, USA},
isbn = 9781595936899,
location = {San Francisco, California, USA},
numpages = 11,
publisher = {Association for Computing Machinery},
series = {POPL '08}
}
|
