Publikation

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.

Abstrakt

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.

Projekte

integer_overflow_detection_in_hardware_designs_at_the_specification_level.pdf (pdf, 367 KB)

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence