Publication
Integer Overflow Detection in Hardware Designs at the Specification Level
Fritjof Bornebusch; Christoph Lüth; Robert Wille; Rolf Drechsler
In: 8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD). International Conference on Model-Driven Engineering and Software Development (MODELSWARD-2020), February 25-27, Valetta, Malta, 2020.
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.