Integer overflow detection in hardware designs at the specification level

Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

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.

Original languageEnglish
Title of host publicationMODELSWARD 2020 - Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development
EditorsSlimane Hammoudi, Luis Ferreira Pires, Bran Selic
PublisherSciTePress
Pages41-48
Number of pages8
ISBN (Electronic)9789897584008
StatePublished - 2020
Externally publishedYes
Event8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020 - Valletta, Malta
Duration: 25 Feb 202027 Feb 2020

Publication series

NameMODELSWARD 2020 - Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development

Conference

Conference8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020
Country/TerritoryMalta
CityValletta
Period25/02/2027/02/20

Keywords

  • Functional HDLs
  • Hardware Designs
  • Hardware Synthesis
  • Integer Overflows
  • Proof Assistants

Fingerprint

Dive into the research topics of 'Integer overflow detection in hardware designs at the specification level'. Together they form a unique fingerprint.

Cite this