Safe secure chips ... http://www.informatik.uni-bremen.de/agra/doc/konf/integer_overflow_detection_in_hardware_designs_at_the_specification_level.pdf Integer Overflow Detection in Hardware Designs at the Specification Level Fritjof Bornebusch1 , Christoph L¨uth1,3 , Robert Wille1,2 , Rolf Drechsler1,3 1Cyber-Physical Systems, DFKI GmbH, Bremen, Germany 2 Integrated Circuit and System Design, Johannes Kepler University Linz, Austria 3Mathematics and Computer Science, University of Bremen, Germany {fritjof.bornebusch,christoph.lueth}@dfki.de, robert.wille@jku.at, drechsler@uni-bremen.de Keywords: Hardware Designs, Integer Overflows, Proof Assistants, Functional HDLs, Hardware Synthesis 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.