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ć (editor). 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.

Projekte

paper.pdf (pdf, 391 KB )

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