Model checking for nonlinear dynamic circuits

• Applicant: Professor Dr.-Ing. Erich Barke
• Subject Area: Electronic Semiconductors, Components and Circuits, Integrated Systems, Sensor Technology, Theoretical Electrical Engineering
• Term: from 2002 to 2006
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5396611

Der vorliegende Antrag umfasst eine Methode zum automatischen Eigenschaftsbeweis (Model-Checking) nichtlinearer dynamischer analoger Schaltungen. Die positiven Erfahrungen, die mit Eigenschaftsbeweisern bei digitalen Schaltungen gemacht wurden motivieren dazu, auch für analoge Schaltungen ein entsprechendes Werkzeug zu entwickeln. Die dazu notwendige Formalisierung des Entwurfsverifikationsprozesses wird zu einer erheblichen Reduzierung der Entwurfsfehler, der notwendigen Redesigns und damit zu einer erheblichen Produktivitätssteigerung im Analogdesign führen. Das zu entwickelnde Werkzeug führt eine speziell auf das nichtlineare dynamische analoge System angepasste Diskretisierung und Relationsberechnung im Zustandsraum durch. Das entstehende Modell wird bezüglich der Eigenschaften geprüft, die in der für diesen Zweck erweiterten Sprache CTL beschrieben werden.

• DFG Programme: Research Grants