PROPERTY DETECTION (FORMAL VERIFICATION) FOR A MIXED SYSTEM OF ANALOG AND DIGITAL SUBSYSTEMS

摘要

The invention relates to a method for detecting properties of a digital-analog mixed signal system (1) by formally verifying a digital substitution system (20). Component parameters and environment parameters are depicted as additional signals in the digital substitution model (substitution model, 20) for the analog components, and the analog part of the system is divided (90) into time-independent and linear time-dependent subsystems. The time-independent subsystems are regarded as stateless and are converted by combinatorial logic and the linear time-dependent subsystems for time-discretization while being substituted by finite automations. Despite the digitizing errors, it is possible to reliably draw conclusions about the original system from the verification results of the substitution model. The properties of the digital-analog mixed signal system (1) that are to be detected are enhanced for the analog components in such a manner that, in all occurring values of digitizing errors, these properties in the digital substitution model are only fulfilled once the digital-analog mixed signal system (1) also fulfills these properties by limiting (92) the permitted range of values for analog signals is limited (92) to twice the amount of the maximum digitizing error.