Publication
Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications
Fritjof Bornebusch; Christoph Lüth; Robert Wille; Rolf Drechsler
In: Slimane Hammoudi; Luís Ferreira Pires; Bran Selić (Hrsg.). 8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), Revised Selected Papers. International Conference on Model-Driven Engineering and Software Development (MODELSWARD-2020), February 25-27, Valletta, Malta, Springer, 2021.
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.