https://www.springerprofessional.de/safety-first-about-the-detection-of-arithmetic-overflows-in-hard/18822316 Authors: Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler 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.