Formalized High Level Synthesis with Applications to Cryptographic Hardware

William Harrison; Ian Blumenfeld; Eric Bond; Chris Hathhorn; Paul Li; May Torrence; Jared Ziegler

doi:10.1007/978-3-031-33170-1_20

Formalized High Level Synthesis with Applications to Cryptographic Hardware

William Harrison
, Ian Blumenfeld
, Eric Bond
, Chris Hathhorn
, Paul Li
, May Torrence
, Jared Ziegler

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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, 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.

Original language	English
Title of host publication	NASA Formal Methods Symposium (NFM23)
Editors	Kristin Yvonne Rozier, Swarat Chaudhuri
Place of Publication	Cham
Publisher	Springer Nature Switzerland
Pages	332-352
Number of pages	21
ISBN (Print)	978-3-031-33170-1
DOIs	https://doi.org/10.1007/978-3-031-33170-1_20
State	Published - Jun 2023
Externally published	Yes
Event	NASA Formal Methods Symposium (NFM23) - Duration: May 16 2023 → May 18 2023 https://conf.researchr.org/home/nfm-2023

Conference

Conference	NASA Formal Methods Symposium (NFM23)
Period	05/16/23 → 05/18/23
Internet address	https://conf.researchr.org/home/nfm-2023

Access to Document

10.1007/978-3-031-33170-1_20

Cite this

@inproceedings{53d8307b80774104a86a0c724e66f5fd,

title = "Formalized High Level Synthesis with Applications to Cryptographic Hardware",

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, 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.",

author = "William Harrison and Ian Blumenfeld and Eric Bond and Chris Hathhorn and Paul Li and May Torrence and Jared Ziegler",

year = "2023",

month = jun,

doi = "10.1007/978-3-031-33170-1\_20",

language = "English",

isbn = "978-3-031-33170-1",

pages = "332--352",

editor = "Rozier, \{Kristin Yvonne\} and Swarat Chaudhuri",

booktitle = "NASA Formal Methods Symposium (NFM23)",

publisher = "Springer Nature Switzerland",

note = "NASA Formal Methods Symposium (NFM23) ; Conference date: 16-05-2023 Through 18-05-2023",

url = "https://conf.researchr.org/home/nfm-2023",

}

Harrison, W, Blumenfeld, I, Bond, E, Hathhorn, C, Li, P, Torrence, M & Ziegler, J 2023, Formalized High Level Synthesis with Applications to Cryptographic Hardware. in KY Rozier & S Chaudhuri (eds), NASA Formal Methods Symposium (NFM23). Springer Nature Switzerland, Cham, pp. 332-352, NASA Formal Methods Symposium (NFM23), 05/16/23. https://doi.org/10.1007/978-3-031-33170-1_20

Formalized High Level Synthesis with Applications to Cryptographic Hardware. / Harrison, William; Blumenfeld, Ian; Bond, Eric et al.
NASA Formal Methods Symposium (NFM23). ed. / Kristin Yvonne Rozier; Swarat Chaudhuri. Cham: Springer Nature Switzerland, 2023. p. 332-352.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formalized High Level Synthesis with Applications to Cryptographic Hardware

AU - Harrison, William

AU - Blumenfeld, Ian

AU - Bond, Eric

AU - Hathhorn, Chris

AU - Li, Paul

AU - Torrence, May

AU - Ziegler, Jared

PY - 2023/6

Y1 - 2023/6

N2 - 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, 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.

AB - 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, 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.

UR - https://harrisonwl.github.io/etc/publications.html

U2 - 10.1007/978-3-031-33170-1_20

DO - 10.1007/978-3-031-33170-1_20

M3 - Conference contribution

SN - 978-3-031-33170-1

SP - 332

EP - 352

BT - NASA Formal Methods Symposium (NFM23)

A2 - Rozier, Kristin Yvonne

A2 - Chaudhuri, Swarat

PB - Springer Nature Switzerland

CY - Cham

T2 - NASA Formal Methods Symposium (NFM23)

Y2 - 16 May 2023 through 18 May 2023

ER -

Formalized High Level Synthesis with Applications to Cryptographic Hardware

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this