Rogin, F.F.RoginKlotz, T.T.KlotzGörschwin, F.F.GörschwinDrechsler, R.R.DrechslerRülke, S.S.Rülke2022-03-102022-03-102008https://publica.fraunhofer.de/handle/publica/35794810.1109/DATE.2008.4484908Property checking is a promising approach to prove the correctness of today's complex designs. However, in practice this requires the formulation of formal properties which is a time consuming and non-trivial task. Therefore the acceptance and efficiency of formal verification techniques can be raised by an automated support for formulating design properties. In this paper we propose a new methodology to automatically generate complex properties for a given design. The tool, Dianosis, implements this methodology by analyzing a simulation trace. The extracted properties describe the abstract design behavior and are presented in a format that is easy to read and can be added to the set of properties used for formal or assertion-based verification. We provide experimental results on industrial hardware designs that show the effectiveness of Dianosis and motivate the practical use.en621conference paper