Integer Overflow Detection in Hardware Designs at the Specification Level
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
Int'l Conf. on Model-Driven Engineering and Software Development (MODELSWARD)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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.
Forschungs-