Automatic Generation of Compact Formal Properties for Effective Error Detection

Several approaches exist in literature for automatic extrac- tion of model behaviours represented in the form of formal properties. Some of them rely on static analysis of the source code, others dynamically mine specifications by analysing simulation traces. In both cases, most of them work at bit level and generate properties in the form of combinational or temporal relationships among Boolean expressions. Such techniques are suited only for gate-level or RTL HW mod- els. There are also approaches working on system-level de- scriptions and SW programs, but they generate properties to express only the sequential ordering of communication function calls and events, while the functional part of the implementation is ignored.To fill in the gap, this paper presents a dynamic method- ology that works on gate-level, RTL and system-level HW descriptions as well as embedded SW, independently from the design model and the abstraction level. The generated properties are in the form of temporal relationships among arithmetic and logic expressions involving traditional HW description language data types (i.e., bit and logic vectors) as well as data types typically adopted in system-level mod- els and SW programs (i.e., integer, double and string). A ranking function is also defined to classify the mined proper- ties according to their capability of capturing meaningful de- sign behaviours. Experimental results have shown that the approach allows generating compact properties really useful to effectively detect errors in the design implementation.