@inproceedings{harrison23,
  title = {Formalized High Level Synthesis with Applications to Cryptographic Hardware},
  author = {Harrison, William L. and Blumenfeld, Ian and Bond, Eric and Hathhorn, Chris and Li, Paul and Torrence, May and Ziegler, Jared},
  booktitle = {NASA Formal Methods Symposium (NFM23)},
  year = {2023},
  abstract = {
  Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, 
the more optimized for performance an accelerator is, the more challenging its verification. This paper introduces a verification methodology, \emph{model validation}, that uses a formalized high-level synthesis language (FHLS) as an intermediary between algorithm specification and hardware implementation. The foundation of our approach to model validation is a mechanized denotational semantics for the ReWire HLS language. Model validation proves the faithfulness of FHLS models to the RTL implementation and we summarize a model validation case study for a suite of pipelined Barrett multipliers.
},
  url_Paper = "https://harrisonwl.github.io/assets/papers/nfm23.pdf",
  url_Slides = "https://harrisonwl.github.io/assets/papers/slides-nfm23.pdf",
}

{"_id":"dBYs37JpsSAgHv3tz","bibbaseid":"harrison-blumenfeld-bond-hathhorn-li-torrence-ziegler-formalizedhighlevelsynthesiswithapplicationstocryptographichardware-2023","author_short":["Harrison, W. L.","Blumenfeld, I.","Bond, E.","Hathhorn, C.","Li, P.","Torrence, M.","Ziegler, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Formalized High Level Synthesis with Applications to Cryptographic Hardware","author":[{"propositions":[],"lastnames":["Harrison"],"firstnames":["William","L."],"suffixes":[]},{"propositions":[],"lastnames":["Blumenfeld"],"firstnames":["Ian"],"suffixes":[]},{"propositions":[],"lastnames":["Bond"],"firstnames":["Eric"],"suffixes":[]},{"propositions":[],"lastnames":["Hathhorn"],"firstnames":["Chris"],"suffixes":[]},{"propositions":[],"lastnames":["Li"],"firstnames":["Paul"],"suffixes":[]},{"propositions":[],"lastnames":["Torrence"],"firstnames":["May"],"suffixes":[]},{"propositions":[],"lastnames":["Ziegler"],"firstnames":["Jared"],"suffixes":[]}],"booktitle":"NASA Formal Methods Symposium (NFM23)","year":"2023","abstract":"Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, the more optimized for performance an accelerator is, the more challenging its verification. This paper introduces a verification methodology, \\emphmodel validation, that uses a formalized high-level synthesis language (FHLS) as an intermediary between algorithm specification and hardware implementation. The foundation of our approach to model validation is a mechanized denotational semantics for the ReWire HLS language. Model validation proves the faithfulness of FHLS models to the RTL implementation and we summarize a model validation case study for a suite of pipelined Barrett multipliers. ","url_paper":"https://harrisonwl.github.io/assets/papers/nfm23.pdf","url_slides":"https://harrisonwl.github.io/assets/papers/slides-nfm23.pdf","bibtex":"@inproceedings{harrison23,\n title = {Formalized High Level Synthesis with Applications to Cryptographic Hardware},\n author = {Harrison, William L. and Blumenfeld, Ian and Bond, Eric and Hathhorn, Chris and Li, Paul and Torrence, May and Ziegler, Jared},\n booktitle = {NASA Formal Methods Symposium (NFM23)},\n year = {2023},\n abstract = {\n Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, \nthe more optimized for performance an accelerator is, the more challenging its verification. This paper introduces a verification methodology, \\emph{model validation}, that uses a formalized high-level synthesis language (FHLS) as an intermediary between algorithm specification and hardware implementation. The foundation of our approach to model validation is a mechanized denotational semantics for the ReWire HLS language. Model validation proves the faithfulness of FHLS models to the RTL implementation and we summarize a model validation case study for a suite of pipelined Barrett multipliers.\n},\n url_Paper = \"https://harrisonwl.github.io/assets/papers/nfm23.pdf\",\n url_Slides = \"https://harrisonwl.github.io/assets/papers/slides-nfm23.pdf\",\n}\n\n","author_short":["Harrison, W. L.","Blumenfeld, I.","Bond, E.","Hathhorn, C.","Li, P.","Torrence, M.","Ziegler, J."],"key":"harrison23","id":"harrison23","bibbaseid":"harrison-blumenfeld-bond-hathhorn-li-torrence-ziegler-formalizedhighlevelsynthesiswithapplicationstocryptographichardware-2023","role":"author","urls":{" paper":"https://harrisonwl.github.io/assets/papers/nfm23.pdf"," slides":"https://harrisonwl.github.io/assets/papers/slides-nfm23.pdf"},"metadata":{"authorlinks":{}},"downloads":8},"bibtype":"inproceedings","biburl":"https://harrisonwl.github.io/assets/bibliography/harrison.bib","dataSources":["wAeScLDKnpPTHdYwg","uCveoExKMHQNZnZCp"],"keywords":[],"search_terms":["formalized","high","level","synthesis","applications","cryptographic","hardware","harrison","blumenfeld","bond","hathhorn","li","torrence","ziegler"],"title":"Formalized High Level Synthesis with Applications to Cryptographic Hardware","year":2023,"downloads":8}