diff options
| -rw-r--r-- | main.tex | 7 | ||||
| -rw-r--r-- | references.bib | 66 |
2 files changed, 51 insertions, 22 deletions
@@ -199,11 +199,14 @@ Using CompCert, we can therefore build a fully verified high-level synthesis too \JW{Some papers to cite somewhere: \begin{itemize} - \item \citet{kundu+08} have done translation validation on an HLS tool called SPARK. - \item \citet{chapman+92} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB: Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.) + \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK.\@ + \item \citet{chapman92_verif_bedroc} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB:\@ Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.) \end{itemize} } + +\YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool. And yes thank you, will definitely cite that paper. There seem to be similar early proofs of high-level synthesis like~\citet{hwang91_formal_approac_to_sched_probl}.} + \section{Verilog Semantics} Definition of state. diff --git a/references.bib b/references.bib index 77ee24c..5ff4450 100644 --- a/references.bib +++ b/references.bib @@ -234,26 +234,52 @@ series = {POPL '08} } -@InProceedings{kundu+08, -author="Kundu, Sudipta -and Lerner, Sorin -and Gupta, Rajesh", -editor="Gupta, Aarti -and Malik, Sharad", -title="Validating High-Level Synthesis", -booktitle="Computer Aided Verification (CAV)", -year="2008", -publisher="Springer", -pages="459--472", +@inproceedings{kundu08_valid_high_level_synth, + author = "Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh", + title = "Validating High-Level Synthesis", + booktitle = "Computer Aided Verification", + year = 2008, + pages = "459--472", + address = "Berlin, Heidelberg", + editor = "Gupta, Aarti and Malik, Sharad", + isbn = "978-3-540-70545-1", + publisher = "Springer", +} + +@inproceedings{chapman92_verif_bedroc, + author = {R. {Chapman} and G. {Brown} and M. {Leeser}}, + title = {Verified high-level synthesis in BEDROC}, + booktitle = {[1992] Proceedings The European Conference on Design Automation}, + year = 1992, + pages = {59--63}, + doi = {10.1109/EDAC.1992.205894}, + month = {March}, + publisher = {IEEE Computer Society}, } -@INPROCEEDINGS {chapman+92, -author = {Richard Chapman and Geoffrey Brown and Miriam Leeser}, -booktitle = {European Conference on Design Automation (EDAC)}, -title = {Verified high-level synthesis in BEDROC}, -year = {1992}, -pages = {59--63}, -doi = {10.1109/EDAC.1992.205894}, -url = {https://doi.ieeecomputersociety.org/10.1109/EDAC.1992.205894}, -publisher = {IEEE Computer Society}, +@article{hwang91_formal_approac_to_sched_probl, + author = {C. -. {Hwang} and J. -. {Lee} and Y. -. {Hsu}}, + title = {A Formal Approach To the Scheduling Problem in High Level + Synthesis}, + tags = {hls}, + journal = {IEEE Transactions on Computer-Aided Design of Integrated + Circuits and Systems}, + volume = 10, + number = 4, + pages = {464-475}, + year = 1991, + doi = {10.1109/43.75629}, + url = {https://doi.org/10.1109/43.75629}, + keywords = {circuit CAD;integer programming;linear + programming;scheduling;integer LP model;CAD;scheduling + problem;high level synthesis;integer linear + programming;time-constrained scheduling;resource-constrained + scheduling;feasible scheduling;chaining;multicycle + operations;nonpipelined function units;pipelined function + units;functional pipelining;loop folding;mutually exclusive + operations;bus constraint;ASAP;ALAP;list scheduling;High level + synthesis;Digital systems;Space exploration;Scheduling + algorithm;Timing;Integer linear programming;Pipeline + processing;Filters;Hardware design languages;Flow graphs}, + month = {April} } |