@inproceedings{336e402fc63f42969cb7be6c37c57dd8,
title = "Integer overflow detection in hardware designs at the specification level",
abstract = "In this work, we present a hardware design approach that allows the detection of integer overflows by describing finite integer types at the specification level. In contrast to the established design flow that uses infinite integer types at the specification level. This causes a semantic gap between these infinite types and the finite integer types used at the model level. The proposed design approach uses dependent types in combination with proof assistants. The combination allows the arguing about the behavior of finite integer types that is used to detect integer overflows at the specification level. To achieve this, we utilized the CompCert integer library that describes finite data types as dependent types.",
keywords = "Functional HDLs, Hardware Designs, Hardware Synthesis, Integer Overflows, Proof Assistants",
author = "Fritjof Bornebusch and Christoph L{\"u}th and Robert Wille and Rolf Drechsler",
note = "Publisher Copyright: Copyright {\textcopyright} 2020 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved.; 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020 ; Conference date: 25-02-2020 Through 27-02-2020",
year = "2020",
language = "English",
series = "MODELSWARD 2020 - Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development",
publisher = "SciTePress",
pages = "41--48",
editor = "Slimane Hammoudi and Pires, {Luis Ferreira} and Bran Selic",
booktitle = "MODELSWARD 2020 - Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development",
}