US 2006/0215743 A1 · Property detection (formal verification) for a mixed system of analog and digital subsystems

Abstract

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.

Claims12

Dependent claims

A method for detecting a property of a digital-analog mixed-signal system (1) by formal verification of a digital substitution system or model (20) characterized in that device parameters and environmental parameters for the analog components are represented as additional signals in the digital substitution model (substitution system;

20) and the analog part of the system is divided into time independent and linear time dependent subsystems (90), wherein the time independent subsystems may be considered as stateless and are replaced by combinatorial logic and wherein the linear time dependent subsystems are replaced by finite automations (2A, 3A) for time discretization and are mapped into the digital substitution model (20), and wherein despite the digitizing error it is possible to draw a reliable conclusion from the verification results of the substitution model with respect to the original system, that is, the properties to be detected of the digital-analog mixed-signal system (1) for the analog components are enhanced in such a way that for all occurring values of the digitizing error this property in the digital substitution model is fulfilled only when the digital-analog mixed-signal system (1) also fulfills this property, by restricting the permitted value range for analog signals by two times the maximum digitizing error (92).

A method for detecting or testing of properties of a digital-analog mixed-signal system (1) by formal verification (95) of a digital substitution model (20), comprising:

(i) mapping device parameters and environmental parameters for analog components of the mixed-signal system (1) into the digital substitution model (20),
(ii) grouping the analog components of the system (1) in at least one time independent subsystem (2) or at least one time dependent (3) subsystem;
(a) said time independent subsystem (group;
2) being regarded as stateless and being replaced by combinatorial logic;
(b) said time dependent subsystem (group;
3) being replaced by a finite automation for a time discretization;
said subsystems being mapped into the digital substitution model (20);
(iii) wherein digitizing errors (11) do not prevent a reliable conclusion regarding the original system (1) from verification results (100) of the substitution model (20), wherein particularly properties to be detected of the digital-analog mixed-signal system (1)—predetermined properties of a reference model (10)—are enhanced (92, 10A) by restricting a permitted value range (a, a′) for analog signals (y(t)) by, particularly, at least two times the amount of the maximum digitizing error (Δ);
(iv) such that for all occurring values of digitizing errors the enhanced properties (A′) are verified as an enhanced reference model (10A) with respect to the digital substitution model (20), wherein the enhanced properties are fulfilled only when the digital-analog mixed-signal system (1) also fulfills the properties of the reference model (10).

6 more elements

Dependencies are inferred from the claim text.

Property detection (formal verification) for a mixed system of analog and digital subsystems

Life of this patent

Property detection (formal verification) for a mixed system of analog and digital subsystems

Life of this patent

Abstract

Claims12