@inproceedings{9ac8ee1cbbc44364b53aefea38c8b417,
title = "Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications",
abstract = "This work proposes an alternative hardware design approach that allows the detection of arithmetic overflows at the specification level. The established hardware design approach describes infinite integer types at that level while the model describes finite types. This opens a semantic gap between both levels, which means that arithmetic overflows cannot be detected at the specification level. To address this problem the CompCert integer library is utilized that describes finite integer types as dependent types using the proof assistant Coq. Properties that argue about these finite types can be specified and verified at the specification level. This closes the semantic gap the established hardware design approach suffers from.",
keywords = "Arithmetic integer overflows, Functional HDLs, Hardware designs, Hardware synthesis, Proof assistants",
author = "Fritjof Bornebusch and Christoph L{\"u}th and Robert Wille and Rolf Drechsler",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020 ; Conference date: 25-02-2020 Through 27-02-2020",
year = "2021",
doi = "10.1007/978-3-030-67445-8\_2",
language = "English",
isbn = "9783030674441",
series = "Communications in Computer and Information Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "26--48",
editor = "Slimane Hammoudi and Pires, \{Lu{\'i}s Ferreira\} and Bran Seli{\'c}",
booktitle = "Model-Driven Engineering and Software Development - 8th International Conference, MODELSWARD 2020, Revised Selected Papers",
}