EP1127323A1

EP1127323A1 - Verfahren und anordnung zum vergleich einer ersten eigenschaft mit vorgegebenen eigenschaften eines technischen systems

Info

Publication number: EP1127323A1
Application number: EP99959229A
Authority: EP
Inventors: Jörg LOHSE; Peter Warkentin
Original assignee: Infineon Technologies AG; Siemens AG; Siemens Corp
Current assignee: Onespin Solutions GmbH
Priority date: 1998-11-03
Filing date: 1999-11-02
Publication date: 2001-08-29
Also published as: JP4418591B2; WO2000026824A1; JP2003503763A; US20020013680A1; US6581026B2

Abstract

Im Rahmen eines Model Checkings wird versucht, eine Eigenschaft an einem technischen System nachzuweisen. Dazu wird ein Vergleich durchgeführt, bei dem mehrere Vergleichsverfahren derart zu koordinieren sind, dass der Vergleich zu einem Ergebnis führt. Insbesondere ist der Vergleich beendet, sobald ein Vergleichsverfahren den Nachweis erbringt, dass die Eigenschaft in dem System vorliegt bzw. dass die dort Eigenschaft nicht enthalten ist.

Description

Beschreibung

Verfahren und Anordnung zum Vergleich einer ersten Eigenschaft mit vorgegebenen Eigenschaften eines technischen Systems

Die Erfindung betrifft ein Verfahren und eine Anordnung zum Vergleich einer ersten Eigenschaft mit vorgegebenen Eigenschaften eines technischen Systems.

Model Checking (MC) ist eine Technik, um Eigenschaften eines technischen Systems mit bestimmten Verfahren zu verifizieren. Beim Einsatz an dem technischen System ergibt sich bisher gelegentlich ein großes Komplexitätsproblem (State Explosion Problem) . Aufgrund dessen werden erhebliche Anstrengungen unternommen, um aus einem zu verifizierenden System einen Teil herauszulösen, der für die Analyse relevant und praktisch verifizierbar ist. Selbst dann scheitert die Verifikation oft an bestehenden Resourcenlimits (Rechenleistung, Speicherplatz) .

Aus [1] ist bekannt, einen Vergleich zweier Schaltungen mittels Binary Decision Diagrams (BDDs) durchzuführen. Insbesondere wird dabei abgestellt auf digitale Schaltkreise hoher Komplexität, die miteinander verglichen werden sollen bzw. für die strukturelle Ähnlichkeiten ermittelt werden (kombinatorische Schaltkreisverifikation) .

Ein erster Ansatz der kombinatorischen Schaltkreisverifikation versucht funktionale Implikationen zu erzeugen, indem Testmuster generiert und auf die zu vergleichenden

Schaltkreise angewandt werden (ATPG-Verfahren) . Dabei wird das Ziel verfolgt, zu beweisen, daß eine Exklusiv-Oder- Funktion zwischen zwei zu vergleichenden Ausgabewerten nicht mit einer logischen "1" belegt werden kann. Ein anderer Ansatz zur kombinatorischen Schaltkreisverifikation beruht auf einer kanonischen Beschreibung Boolescher Funktionen. Eine solche kanonische Beschreibung wird dargestellt durch BDDs oder spezielle Varianten der BDDs, z.B. durch Reduced Ordered BDDs (ROBDDs), vergleiche insbesondere [2] . Ein spezielles Problem der BDDs ist ihr exponentiell steigender Speicherplatzbedarf.

Ein sogenanntes SAT-Vergleichsverfahren (auch: SAT- Vergleicher; SAT = "Satisfiability") ist aus [3], [4] oder. [7] bekannt. Das SAT-Vergleichsverfahren zeichnet sich dadurch aus, daß für beliebige Boolesche Notationen der Form

(ki v k₂) Λ (k₃ v k₅) Λ (k₂ v k₄) (1)

systematisch Lösungen gesucht werden. Ist bei der Suche der gesamte Suchraum ausgeschöpft und keine Lösung gefunden, so ist das zugrundeliegende Boolesche Problem nicht lösbar.

Die der Erfindung zugrundeliegende Aufgabe besteht darin, eine erste Eigenschaft mit vorgegebenen Eigenschaften eines technischen Systems zu vergleichen, wobei insbesondere eine automatische Lösung des Vergleichsproblems sichergestellt wird.

Diese Aufgabe wird gemäß den Merkmalen der unabhängigen Patentansprüche gelöst. Weiterbildungen der Erfindung ergeben sich auch aus den abhängigen Ansprüchen.

Zur Lösung der Aufgabe wird ein Verfahren zum Vergleich einer ersten Eigenschaft mit vorgegebenen Eigenschaften eines technischen Systems angegeben, bei dem mindestens zwei Vergleichsverfahren vorgesehen sind, deren jedes einen Vergleich der ersten Eigenschaft mit den vorgegebenen Eigenschaften des technischen Systems durchführen kann. Die mindestens zwei Vergleichsverfahren werden in einer vorgegebenen Reihenfolge solange abgearbeitet, bis ein Ergebnis des Vergleichs bestimmt wird. Dabei ist es insbesondere von Vorteil, daß automatisch unterschiedliche Vergleichsverfahren abgearbeitet werden.

Eine Weiterbildung besteht darin, daß das Ergebnis der Vergleichs eine Gleichheit oder eine Verschiedenheit der ersten Eigenschaft von den Eigenschaften des technischen Systems ist.

Insbesondere kann der Vergleich abgebrochen werden, sobald eine einzelne Verschiedenheit entdeckt wird.

Eine andere Weiterbildung sieht vor, daß anhand der Gleichheit die erste Eigenschaft durch das technische System verifiziert wird.

Bei den mindestens zwei Vergleichsverfahren kann es sich insbesondere um zwei der folgenden Vergleichsverfahren handeln: a) SAT-Vergleichsverfahren; b) Simulationsverfahren; c) BDD-Verfahren; d) ATPG-Verfahren; e) Verfahren basierend auf internen Äquivalenzpunkten.

Insbesondere kann das BDD-Verfahren ein ROBDD-Verfahren sein. Weiterhin kann das ROBDD-Verfahren bezüglich seiner Blätter oder bezüglich der Schnittebenen durchgeführt werden.

Das technische System kann eine Schaltung, insbesondere eine elektrische Digitalschaltung sein.

Weiterhin ist es möglich, zumindest einen Teil des Vergleichs durchzuführen, wobei ein Zwischenergebnis eine Komplexität des gesamten Vergleichs reduziert. Durch eine auf diese Art reduzierte Komplexität kann mittels eines Vergleichsverfahrens, das ursprünglich an dem gesamten Vergleich scheiterte, ein Ergebnis erzielbar sein. Weiterhin ist es möglich, das Zwischenergebnis eines Vergleichsverfahrens, das nicht zu Ende durchführbar war, in einem weiteren Vergleichsverfahren zu nutzen (Ausnutzung von Seiteneffekten) . So bietet ein abgebrochenes BDD-

Vergleichsverfahren einen Ansatz zur Darstellung des zu lösenden Problems (hier: des gesamten Vergleichs) . Dieser wird in einem anderen Vergleichsverfahren aufgegriffen als Zwischenergebnis, was in einer Einsparung von Rechenzeit und/oder Speicherplatz resultiert.

Ergibt ein Vergleich als Ergebnis Ungleichheit, so werden bevorzugt Diagnoseinformationen dargestellt, die es einem Benutzer ermöglichen, die Ursache für die Ungleichheit zu ermitteln.

Im Rahmen einer Weiterbildung wird das technische System als ein endlicher Automat beschrieben. Ferner kann die erste Eigenschaft als eine Boolesche Funktion dargestellt sein. Zusätzlich kann durch die erste Eigenschaft ein Verhalten des technischen Systems über einem vorgegebenen Zeitintervall beschrieben sein.

Digitale Schaltungen werden zunehmend größer. Ein Test auf korrektes Verhalten wird damit komplexer, zeitaufwendiger und teurer. MC für Schaltungen realer Größe ist damit ein entscheidender ökonomischer Faktor. Durch das vorgestellte Verfahren und die zugehörige Anordnung wird die Handhabbarkeit der Technik für den Nutzer erheblich vereinfacht. Der hier beschriebene Ansatz beschränkt sich nicht auf einen Hardware-Entwurf, sondern kann auch zur Verifikation von Software, deren Verhalten bevorzugt durch einen endlichen Automaten beschreibbar ist (z.B. SDL- Programme, Protokolle) , eingesetzt werden.

Im vorliegenden Ansatz kann ein hybrider Beweiser, d.h. ein Prozeß mit mehreren Vergleichsverfahren, zur Lösung einer Verifikationsaufgabe eingesetzt werden. Ein hybrider Beweiser ist ein Rahmenwerk, welches eine Menge von Teilbeweisern (einzelne Vergleichsverfahren) enthält. Der hybride Beweiser koordiniert die Arbeitsweise der Teilbeweiser . Ziel ist es, durch den Einsatz verschiedener Beweiser Verifikationsaufgaben zu lösen, die kein Beweiser alleine gelöst haben würde. Kann keiner der Teilbeweiser eine gegebene Verifikationsaufgabe lösen, so wird die diese Verifikationsaufgabe zerlegt. Dazu werden jedem Teilbeweiser Unteraufgaben übertragen, die er unter Vorgabe von Ressourcen bearbeiten kann. Bei Überschreitung eines Schwellwertes für die Belegung zugehöriger Ressourcen, bricht der Beweiser seine Bearbeitung ab. Der hybride Beweiser entscheidet dann, ob die Unteraufgabe von einem anderen Teilbeweiser behandelt wird, ob die Ressourcen erhöht werden sollen oder ob mit einer anderen Unteraufgabe fortgefahren wird.

Im Rahmen einer zusätzlichen Ausgestaltung wird für jedes Vergleichsverfahren ein Schwellwert für bereitzustellende Ressourcen (z.B. Speicherplatz oder Rechenleistung) und/oder zur Durchführung des Vergleichsverfahrens bereitzustellende Zeit bestimmt, wobei bei Überschreitung des Schwellwerts das jeweilige Vergleichsverfahren als nicht erfolgreich beendet wird.

Dies ist besonders dann von Vorteil, wenn ein einzelnes Vergleichsverfahren, z.B. durch schnell ansteigende Komplexität, einen Rechner, auf dem es abläuft, blockiert oder keine Lösung in einem vorgegebenen Zeitintervall bestimmt wird. In so einem Fall ist es oft besser, eine Lösung mit dem nächsten Vergleichsverfahren zu erwirken.

Auch ist es eine Weiterbildung, daß die Reihenfolge der durchzuführenden Vergleichsverfahren dynamisch angepaßt wird. Dies geschieht bevorzugt dadurch, daß mitprotokolliert wird, welches Vergleichsverfahren die meisten Ergebnisse bestimmt hat, wobei dieses "beste" Vergleichsverfahren für zukünftige Vergleiche als erstes eingesetzt wird. Entsprechend erfolgt eine Sortierung der Reihenfolge mit dem "zweitbesten", dem "drittbesten", usf. Vergleichsverfahren.

Das Ergebnis des Vergleichs kann eingesetzt werden, um einen Entwurf, eine Anpassung oder eine Steuerung des technischen Systems durchzuführen.

Insbesondere bei der Schaltkreissimulation kann das Ergebnis des beschriebenen Vergleichs, so es positiv ist, direkt umgesetzt werden, indem eine vorgegebene Beschreibungsform einen Produktionsprozeß des Schaltkreises einleitet.

Zur Lösung der Aufgabe wird weiterhin eine Anordnung zum Vergleich einer ersten Eigenschaft mit vorgegebenen

Eigenschaften eines technischen Systems, angegeben, die eine Prozessoreinheit aufweist, die derart eingerichtet ist, daß a) mindestens zwei Vergleichsverfahren vorgesehen sind, deren jedes einen Vergleich der ersten Eigenschaft mit den vorgegebenen Eigenschaften des technischen Systems durchführen kann; b) die mindestens zwei Vergleichsverfahren in einer vorgegebenen Reihenfolge solange abarbeitet, bis ein Ergebnis des Vergleichs bestimmbar ist.

Diese Anordnung ist insbesondere geeignet zur Durchführung des erfindungsgemäßen Verfahrens oder einer seiner vorstehend erläuterten Weiterbildungen.

Ausführungsbeispiele der Erfindung werden nachfolgend anhand der Zeichnung dargestellt und erläutert.

Es zeigen

Fig.l ein Blockdiagramm für die Arbeitsweise eines hybriden Beweiser; Fig.2 ein Blockdiagramm für die Auswahl elementarer Beweiser als Teile eines hybriden Beweisers;

Fig.3 ein Blockdiagramm für einen Beweiser für interne Äquivalenzpunkte;

Fig.4 ein Blockdiagramm, das die Durchführung einer vollständigen Simulation veranschaulicht;

Fig.5 ein Blockdiagramm mit Schritten eines ROBDD- Beweisverfahrens;

Fig.6 eine Prozessoreinheit.

Eine Vorgehensweise beim Model Checking (MC) ist insbesondere wie folgt:

• das technische System wird als ein endlicher Automat dargestellt; • eine Eigenschaft beschreibt das Verhalten des technischen Systems über einem endlichen Zeitintervall;

• die Eigenschaft wird als Boolesche Funktion dargestellt; • die Verifikationsaufgabe wird auf den Beweis der

Gleichheit von Booleschen Funktionen zurückgeführt;

• die Gleichheit von zwei Booleschen Funktionen wird mit einem hybriden Vergleicher gelöst.

EIGENSCHAFTEN

Eigenschaften beschreiben das Verhalten eines technischen Systems über eine vorgegebene endliche Anzahl von Zeitpunkten (=Invarianten über einem endlichen Zeitintervall) . Ausgehend von einer Menge von atomaren Aussagen (AA) wird eine mögliche Eigenschaftssprache definiert. Eine elementare Aussage (EA) (state expression) ist eine beliebige Boolesche Verknüpfung von AA.

Im folgenden sei t ein beliebiger fester Zeitpunkt. Eigenschaften werden mit Referenz auf diesen Zeitpunkt formuliert.

Eine elementare Aussage zum Zeitpunkt t+k (EA ) (timed State expression; k ist eine ganze Zahl größer gleich 0) ist ein Ausdruck der Gestalt

at t+k: EA ( 2 :

Eine Eigenschaft (über n Zeitpunkte) ist eine Boolesche Verknüpfung von endlich vielen zeitbehafteten elementaren Aussagen

EA mit k < n (3)

Um Eigenschaften (besser) zu strukturieren, kann man sie in einen Annahmeteil (assume) und einen Beweisteil (prove) unterteilen; dies ist gleichbedeutend mit der Implikation

assume => prove (4) .

Beispiel für eine Eigenschaft:

assume: at t+0: not reset and at t+1: not reset;

prove: at t+0: request implies at t+1: acknowledge

Hierbei sind "reset", "request", "acknowledge" atomare Aussagen. Die Eigenschaft drückt aus, daß unter der Voraussetzung "not reset" ein "request" (zum Zeitpunkt 0) nach einem Zeitschritt mit einem "acknowledge" quittiert wird.

SEMANTIK

Nachfolgend werden insbesondere technische Systeme betrachtet, die als endliche Automaten darstellbar sind. Derartige Systeme sind bspw. Schaltungen (in Form von VHDL- Programmen oder EDIF-Netzlisten) . Ein endlicher, deterministischer Automat ist ein 5-Tupel der Form

(S, I, T, MAA, P) (5) ,

wobei

S eine endliche Menge von Zuständen,

I eine endliche Menge von Eingabesymbolen,

T c: S x I x S eine Übergangsrelation,

MAA eine Menge von atomaren Aussagen (AA) und P: S x I -» Potenzmenge (MAA) eine Bewertungsfunktion bezeichnen.

Die Bewertungsfunktion P gibt an, welche atomaren Aussagen (AA) in einem Zustand erfüllt sind.

Vereinbart wird eine charakteristische Funktion χ_j? einer Eigenschaft E. Die charakteristische Funktion χ_jr wird eingesetzt, um eine Gültigkeit der Eigenschaft E zu bestimmen.

Es seien AA eine atomare Aussage und B = {0,1} die Boolesche Menge. Die charakteristische Funktion χj wird definiert durch

_χAA:S x I → B (6)

mit XAÄ(^S' i) ⁼ 1 genau dann wenn AA e P(s, i), d.h. AA ist in (s,i) erfüllt. Weiterhin sei

EA = B(AA]_, ... , AA_m) (7)

eine Boolesche Verknüpfung von atomaren Aussagen (d.h. eine elementare Aussage). Somit wird definiert:

XEA = ^B(λAA! > ^{■ ■ ■} > XAA_m ) (8)

Nachfolgend werden Aussagen betrachtet, die sich auf mehrere Zustände beziehen. Es gelte

σ = ((s₀, in), • • • , (sn-l, in-l)) e (S x if ⁽9⁾

und

σ (^sk, ik) (10)

und E sei eine Eigenschaft über n Zeitpunkte. Die charakteristische Funktion χjr ist eine Funktion

mit

λE(^σ) = XEA(σ^k) (12)

falls

E = EA^k (13)

eine elementare Aussage ist, und

falls

eine Boolesche Verknüpfung von elementaren Aussagen ist.

Eigenschaften (über n Zeitpunkte) werden über Pfade (der Länge n) eines Automaten interpretiert. Es sei

χ_τ: S x I x S → B (16)

die charakteristische Funktion der Übergangsrelation T. σ bezeichnet einen Pfad der Länge n, wenn s_k+ι ein Nachfolgezustand von s_k ist, d.h. wenn gilt

(s_k, i_k, s_{k + 1}) e T (17)

oder

Xτ(^sk' ik, ^sk+l) = ^{1 für} k=0,l, ... ,n-2 (n > 2) (18)

Daraus folgt:

XPfad(^σ) = Xτ(^s0 iO' ^sl) ^{Λ ■ • • Λ} Xτ(^sn-2' n-2 ^sn-l) (19)

Eine Eigenschaft E über n Zeitpunkte ist erfüllt genau dann wenn gilt:

(Xpfad => Xε)(σ) = 1 : 2o :

für alle Pfade σ der Länge n. Ein Gegenbeispiel zur Eigenschaft E ist eine Belegung an, so daß gilt

(Xpfad ^Λ notχ_EXσ₀) = 1 (21) .

Die nachfolgend vorgestellten Methoden können auf beliebige Funktionen gemäß Gleichung (11) angewandt werden. Die vorgestellte Eigenschaftssprache stellt nur eine mögliche Instanz dar, um Eigenschaften zu beschreiben. Ebenso wäre es möglich, den Definitionsbereich (s x ϊf¹ zu erweitern, z.B. zu

(s x if¹ x S, um eine mächtigere Sprache zu definieren.

Im weiteren wird von einer binären Kodierung des endlichen Automaten ausgegangen, d.h.

Die Verifikation ist damit auf den Beweis der Gleichheit einer Booleschen Funktion mit der konstanten Funktion 1 zurückgeführt.

SPEZIALFALL: KOMBINATORISCHER VERGLEICH

Beim kombinatorischen Vergleich werden zwei endliche, deterministische Automaten mit Ausgabe miteinander verglichen. Diese Automaten können z.B. zwei digitale Schaltungen darstellen. Ein endlicher, deterministischer Automat mit Ausgabe ist ein 5-Tupel

(S, I, 0, δ, λ) (23),

wobei

S eine endliche Menge von Zuständen, I eine endliche Menge von Eingabesymbolen,

0 eine endliche Menge von Ausgabesymbolen, δ: S x I —> S die Übergangsfunktion, λ: S x I — 0 die Ausgabefunktion bezeichnen.

Es seien

Mi = (Si, I_if O_if δ_i λ_±) mit i=l,2 (24 )_

zwei endliche, deterministische Automaten mit Ausgabe. Unter einer gemeinsamen Kodierung von Mι_, M₂ werden bijektive Abbildungen

^bij_s ^{: S}l → S₂, bij_jili → I₂ , ^: Oχ → 0₂ (25)

wobei mit 'b j' eine Bijektion bezeichnet wird, verstanden.

Die Automaten Mi, M₂ heißen kombinatorisch äquivalent bzgl. einer gemeinsamen Kodierung gemäß Gleichung (25) genau dann, wenn gilt

bij_s(δι(s,i)) = δ₂(b_ijs(s),b_ij₁(i)) (26)

und

b_iJQ(λι(s,i)) = λ₂(b_ijs(s)b_ijl(i)) (27)

für alle s e Sι_ , i e I]_ . Nach Identifikation von

Si = Ξ₂ = S, Ii = I₂ = I, Oi = 0₂ = 0 (28)

ergeben sich daraus die Bedingungen

δι(s,i) = δ₂(s, i) (29)

und λ!(s, i) = λ₂(s, i) ( 30 ) .

für alle s e S]_ und i e I]_ .

Eine binäre Kodierung von S, I, 0 überführt dies in eine (endliche) Anzahl von Gleichheitsrelationen zwischen Booleschen Funktionen.

BEWEISER

Es seien

Flj, 2j, j=l,2,...,n (31;

Boolesche Funktionen. Zur Behandlung des Problems

"Gilt Fij ≡ F₂j für j=l, 2, ... , n?" (321

gibt es unterschiedliche Methoden (Vergleichsverfahren) . Jede Methode hat dabei eigene Stärken und Schwächen. Durch Nutzung einer geeigneten Auswahl solcher Methoden werden die Schwächen einzelner Methoden eliminiert und damit die Robustheit des Lösungsansatzes deutlich erhöht. Durch überlappende Anwendung der Methoden können deutlich größere Systeme verglichen werden, als dies mit je einer einzelnen Methode möglich wäre.

In einem ersten Schritt werden die Funktionen nach Gleichung (31) durch einen gerichteten azyklischen Graphen dargestellt. Auf dieser Graphenstruktur setzen die einzelnen Methoden, auch als Teilbeweiser bezeichnet, auf.

Ein gerichteter, azyklischer Graph ist eine Menge K von Knoten und eine Menge ( c K x K ) von gerichteten Kanten, die jeweils zwei Knoten miteinander verbinden. Der Graph umfaßt keine Zyklen. Ein Knoten k₂ heißt Sohn des Knotens ki, falls eine gerichtete Kante den Knoten k mit dem Knoten k₂ verbindet. Blätter sind Knoten, von denen keine Kanten ausgehen. Wurzeln sind Knoten, in die keine Kanten münden. Gerichtete Kanten verlaufen von oben nach unten, so daß Wurzeln ganz oben und Blätter ganz unten im Graphen liegen.

Unter einer Basis (auch: Schnittebene) eines Graphen wird eine Teilmenge von Knoten mit der Eigenschaft "jeder Pfad von einer Wurzel zu einem Blatt läuft durch einen Knoten der Basis" verstanden. Insbesondere bildet die Menge aller

Blätter eine Basis. In [5] wird ein Algorithmus beschrieben, mit dessen Hilfe eine Basis bestimmbar ist.

Sei k ein Knoten in der Graphenstruktur G. Der sogenannte Abhängigkeitskegel (engl.: Cone of Influence) von k ist die kleinste Substruktur G_k von G für die gilt: der Knoten k gehört zu G_k und mit einem Knoten k' gehören auch alle Söhne von k' zu G_k.

Mit folgender Interpretation stellt ein gerichteter, azyklischer Graph eine Boolesche Funktion dar: Jedem von einem Blatt verschiedenen Knoten k ist eine Boolesche Operation op_k zugeordnet. Die Söhne des Knotens k sind die Operanden von op_k. Blätter (Wurzeln) stellen die Argumente (den Wert) der Booleschen Funktion dar. Ein Blatt kann auch eine Konstante mit einem Wert "0" oder einem Wert "1" sein. Jeder Knoten der Graphenstruktur G repräsentiert eine Boolesche Funktion boole_k, die von den primären Eingängen abhängig ist. Die Darstellung einer Booleschen Funktion als Graph ist nicht kanonisch, d.h. es gibt i.a. viele unterschiedliche Darstellungen. Knoten, welche dieselbe Boolesche Funktion darstellen, heißen äquivalent.

Um eine kompakte Darstellung zu erhalten, dürfen Kanten markiert sein, um einstellige Operationen, z.B. not, zu symbolisieren. Beispielsweise wird in [1] in den Knoten nur eine zweistellige and-Operation zugelassen. Die (einstellige) not-Operation wird durch Markierung der Kante gekennzeichnet.

Beim Aufbau des Graphen wird über eine Hashtabeile die Eindeutigkeit eines Knotens sichergestellt. Nach jeder Veränderung des Graphen (d.h. Zusammenlegung von zwei oder mehreren verschiedenen, äquivalenten Knoten) werden mehrfach auftretende identische Knoten zusammengelegt; somit bleibt die Eindeutigkeit eines Knotens erhalten. Dieser Vorgang heißt Rehashing.

Eine Aufgabe der Beweiser ist es, den zugrundeliegenden Graphen zu vereinfachen bis Problem (32) lösbar ist: In verschiedenen Phasen des Verfahrens werden Knoten bestimmt, die die gleiche Funktion darstellen, also äquivalent sind. Unter diesen Knoten wird dann ein Knoten als Repräsentant ausgewählt, alle anderen Knoten werden durch diesen Repräsentanten ersetzt. Dieser Prozeß heißt Elimination redundanter Knoten. Unmittelbar nach einer Elimination wird jedesmal ein Rehashing durchgeführt.

Zu Beginn eines jeden Beweisschritts, um beispielsweise eine Gleichheit

boole_kl = boolej₂ (33)

für zwei verschiedene Knoten k]_, k₂ nachzuweisen, wird zuerst der "Cone of Influence" der beteiligten Knoten bestimmt und dann auf diesem "Cone of Influence" weitergerechnet.

Im folgenden wird eine mögliche Auswahl von

Methoden/Beweisern vorgestellt, die in einer Implementierung genutzt werden. Dies sind:

• vollständige Simulation; • ROBDD-Verfahren (bzgl. Blätter);

• ROBDD-Verfahren (bzgl. Schnittebenen);

• ATPG-Verfahren (Automatische Testmustergenerierung) ; • SAT-Verfahren (Boolesche Erfüllbarkeitsalgorithmen) ;

• Beweiser für interne Äquivalenzpunkte.

Auf die einzelnen Beweiser/Methoden wird nachfolgend detailliert eingegangen.

SIMULATION

Die Simulation (vergleiche [6]) erfolgt von den Blättern zu den Wurzeln: Zuerst wird jedem Blatt ein Wert "0" oder "1" zugeordnet. Ist jedem Sohn eines Knoten k ein Wert zugeordnet worden, so wird der Wert des Knotens k mittels der Operation op_k bestimmt.

ROBDDS

ROBDDs (Reduced Ordered Binary Decision Diagrams, (siehe [2]) stellen eine Boolesche Funktion als azyklischen Graphen dar. Für eine gegebene Permutation der Argumente, die Variablenordnung, ist diese Darstellung eindeutig. Die Variablenordnung ist in vielen Fällen entscheidend für die Größe des Graphen. Ist es möglich, die Boolesche Funktion als ROBDD (unter Berücksichtigung bestehender Restriktionen an Speicher und Laufzeit) darzustellen, so ist auf Grund der Eindeutigkeit der Darstellung die Frage der Gleichheit verschiedener technischer Systeme unmittelbar gelöst. Der Erfolg dieser Methode hängt von der Booleschen Funktion und der gewählten Variablenordnung ab.

Die Berechnung eines ROBDDs für die Wurzeln eines Graphen G geht von einer Basis (Schnittebene) des Graphen G aus und schreitet in Richtung der Wurzeln fort. Zuerst wird jedem Basisknoten eine BDD-Variable zugeordnet. Dies ist von Bedeutung, da insbesondere durch diese Zuordnung die Variablenordnung festgelegt wird. Sind die ROBDDs für alle Söhne eines Knotens k berechnet, kann auch das ROBDD des Knotens k erzeugt werden. Überschreitet die Größe eines ROBDD eine vorgegebene Schranke, wird die ROBDD Generierung abgebrochen. (In [1] wird dem Knoten eine neue Variable zugeordnet und weitergerechnet.)

ROBDDs ist der Hauptvertreter aus einer Reihe von ähnlichen Darstellungen für Boolesche Funktionen (vergleiche insbesondere [2]). Jede der dort angeführten Darstellungen kann hier eingesetzt werden.

EIN HYBRIDER BEWEISER

Um die Aussage (32) entscheiden zu können, werden die Booleschen Funktionen (31) durch einen gerichteten, azyklischen Graphen G dargestellt. Zu jeder Funktion Fj_j gibt es in dem Graphen G einen Knoten kj_j, der Fj_j repräsentiert. Die Gleichungen Fj ≡ F₂j werden nun sortiert bzgl. des

Abstandes des entsprechenden Knotenpaares (kι_j, k₂j) von den

Blättern des Graphen G. Der hybride Beweiser wird nacheinander für jedes Knotenpaar (kι_j, k₂jl aufgerufen, beginnend mit Knotenpaaren nahe bei den Blättern.

In Fig.l ist ein hybrider Beweiser dargestellt. Als Eingabe in den Beweiser dienen zwei Knoten k , k₂ des Graphen G (vergleiche Block 1 in Fig.l). Ziel ist es, zu entscheiden, ob die durch die Knoten k , k dargestellten Funktionen boolek-, , boole_k;? identisch sind, d.h. ob

boole_k-, ≡ boole_k? (34)

gilt. Der Graph G stellt eine globale Datenstruktur dar, auf die jeder Teilbeweiser (elementarer Beweiser, siehe Block 102 und Fig.2) zugreifen kann. Die Teilbeweiser versuchen, den Graphen G durch Zusammenlegung äquivalenter Knoten schrittweise zu vereinfachen, so daß schließlich, z.B. mittels vollständiger Simulation, die Gleichung (34) bewiesen oder widerlegt werden kann.

Im folgenden bezeichnet C0I(kι,k₂) den "Cone of Influence". von ki, k₂ in dem Graphen G.

Führen die Teilbeweiser, subsummiert unter Block 102 in

Fig.l, nicht zum Erfolg, so erfolgt in einem Block 103 ein Beweisverfahren für interne Äquivalenzpunkte (siehe auch Fig.3). Jeder einzelne Beweiser kann die Ergebnisse "FALSCH" 104, d.h. die zu vergleichenden technischen Systeme sind verschieden, "WAHR" 106, falls die Systeme gleich sind, oder "OFFEN" 105, falls der Beweiser nicht zu einem Ergebnis kommen konnte, liefern.

Nachfolgend werden einzelne Durchführungsschritte des hybriden Beweisers dargestellt und erläutert.

Schritt 1: Vollständige Simulation, siehe Fig.2, Block 201 und Fig.4:

Für 'kleine' COI(kι,k₂) (siehe Block 401): Alle möglichen Wertebelegungen werden simuliert und daraufhin getestet, ob sie die Gleichung (34) erfüllen oder nicht (siehe Block 402) .

Schritt 2: ROBDDs bezüglich Blätter, siehe Block 202: Wähle als Basis die Menge aller Blätter von COI(k ,k₂). Berechne ROBDDs auf COI(k ,k₂) bis zu einer vorgegebenen Größe. Falls in C0I(kι,k₂) redundante Knoten vorhanden sind, also Knoten mit gleicher ROBDD-Darstellung auftreten, werden diese redundante Knoten eliminiert, und es wird Schritt 2 wiederholt. Schritt 3: ROBDDs bezüglich Schnittebenen, siehe Block 203 und Fig.5:

Wähle als Basis eine Menge von Knoten 'nahe' bei den Wurzeln k , k (siehe [5]). Berechne ROBDDs auf COI(kι,k₂) bis zu einer vorgegebenen Größe (siehe Block 501). Falls in COI(k ,k₂) redundante Knoten, d.h. Knoten mit gleicher ROBDD-Darstellung auftreten, werden diese .. redundanten Knoten eliminiert (siehe Block 502) .

Falls die gewählte Basis nicht nur aus Blättern besteht

(siehe Block 503) , kann eine gefundene Widerlegung falsch sein, denn die Basisknoten können voneinander abhängig sein (false negatives) .

Durch Verschiebung der Basis in Richtung zu den Blättern (siehe Block 504) wird Schritt 3 wiederholt.

Erst wenn die Berechnung der ROBDDs zu groß wird, die Gleichung (34) bewiesen ist oder die Basis gänzlich aus Blättern besteht, wird Schritt 3 beendet (siehe Blöcke 505 und 506) .

Schritt 4: ATPG, siehe Block 204:

Die Frage, ob eine Boolesche Funktion den Wert "0" oder "1" annimmt, bzw. die Frage nach der Gleichheit zweier Boolescher Funktionen, läßt sich als Problem im Bereich der automatischen Testmustergenerierung (Automatic Test Pattern Generation - ATPG) formulieren.

Schritt 5: SAT, siehe Block 205:

Die Aussage (34) wird in eine konjunktive Normalform überführt und einem SAT-Beweiser (z.B. [3] oder [4]) übergeben.

Schritt 6: Beweiser für interne Äquivalenzpunkte, siehe Block 103 und Fig.3: Schritt 6.1: (RPS - Random Pattern Simulation): Die Knoten der Graphenstruktur G werden in Äquivalenzklassen zerlegt (siehe Block 301) : Ausgehend von einer Zerlegung {K} wird durch einen Simulationsschritt eine bestehende Zerlegung verfeinert. Dabei wird eine Klasse AK zerlegt in zwei Teilklassen AKn, AK , wobei AKi die Menge aller Knoten e AK darstellt, denen durch die Simulation der Wert i zugeordnet wird. Die Simulation benutzt einen Zufallsgenerator für die Wertebelegung der

Blätter (Random Pattern Simulation = RPS) . Dieser Verfeinerungsschritt wird mehrmals durchlaufen.

Eine Äquivalenzklasse stellt eine Menge von Knoten dar, die potentiell die gleiche Funktion darstellen.

Knoten aus unterschiedlichen Äquivalenzklassen können nicht dieselbe Funktion darstellen.

Schritt 6.2: Nacheinander werden alle potentiell äquivalenten

Knotenpaare auf tatsächliche Äquivalenz untersucht, d.h. es wird geprüft, ob sie dieselbe Boolesche Funktion darstellen (siehe Blöcke 302, 303 und 304) .

Es wird jeweils das noch nicht behandelte, potentiell äquivalente Knotenpaar (u ,u₂) bestimmt, daß am 'nächsten' bei den Blättern liegt (siehe Block 305). Für dieses Knotenpaar (u ,u₂) werden die Schritte 1-5 durchlaufen (siehe Block 306) . Danach ergibt sich eines der drei Ergebnisse:

a. das Knotenpaar (uι,u₂) ist tatsächlich äquivalent: ein Knoten ist redundant und kann eliminiert werden (siehe Block 307); b. das Knotenpaar (u ,u₂) ist nicht äquivalent: es wurde ein Belegung der Variablen (Blätter des "Cone of Influence" von ui, u ) gefunden, an der sich die beiden Funktionen boole_Ul und boole_u„ unterscheiden. Nach Zuweisung von Zufallswerten für die restlichen Blätter des Graphen G, wird der Graph G simuliert und die bisherige Äquivalenzklassenzerlegung verfeinert. Dies vermindert die Anzahl von potentiell äquivalenten Knotenpaaren (siehe Block 308) ; c. der Äquivalenznachweis ist wegen

Komplexitätsgrenzen nicht entscheidbar: es wird das nächste Knotenpaar überprüft.

Nach jeder Überprüfung eines potentiell äquivalenten Knotenpaares wird getestet, ob das ursprüngliche Knotenpaar (ki, k₂) äquivalent ist. Falls dies nicht der Fall ist, wird im letzten Schritt das Knotenpaar

(ki, k₂) getestet.

In Fig.6 ist eine Prozessoreinheit PRZE dargestellt. Die Prozessoreinheit PRZE umfaßt einen Prozessor CPU, einen Speicher SPE und eine Input/Output-Schnittstelle IOS, die über ein Interface IFC auf unterschiedliche Art und Weise genutzt wird: Über eine Grafikschnittstelle wird eine Ausgabe auf einem Monitor MON sichtbar und/oder auf einem Drucker PRT ausgegeben. Eine Eingabe erfolgt über eine Maus MAS oder eine Tastatur TAST. Auch verfügt die Prozessoreinheit PRZE über einen Datenbus BUS, der die Verbindung von einem Speicher MEM, dem Prozessor CPU und der Input/Output-Schnittstelle IOS gewährleistet. Weiterhin sind an den Datenbus BUS zusätzliche Komponenten anschließbar, z.B. zusätzlicher Speicher, Datenspeicher (Festplatte) oder Scanner. Literaturverzeichnis :

[1] A. Kuehlmann, F. Krohm: "Equivalence Checking Using Cuts and Heaps", 34^th ACM/IEEE Design Automation Conference, 1997, pp.263-268.

[2] J. Jain, N. Narayan, M. Fujita, A. Sangiovanni- Vincentelli: "A Survey of Techniques for Formal Verification of Combinational Circuits", Proc. Int. Conf. On Computer Design (ICCD), 1997, pp.445-454.

[3] J. P. M. Silva: "An Overview of Backtrack Search Satisfiability Algorithms", 5^th Int. Symposium on Artificial Intelligence and Mathematics, 1998.

[4] R. J. Bayardo Jr . , R.C. Schräg: "Using CSP Look-Back

Techniques to Solve Real-World SAT-Instances" , Proc. Of the National Conf. On Artificial Intelligence, pp.203- 208, July 1997.

[5] Y. Matsunaga: "An Efficient Equivalenc Checker for

Combinational Circuits", 33^rd ACM/IEEE Design Automation Conference, 1996, pp.629-634.

[6] F. Krohm, A. Kühlmann, A. Mets: "The Use of Random Simulation in Formal Verification", Proc. Int. Conf. on Computer Design (ICCD), 1996, pp.371-376.

[7] M. Davis, H. Putnam: "A Computing Procedure for

Quantification Theory", Journal or the Association for Computing Machinery, Vol.7, Number 3, July 1960, pp.125-139.

Claims

Patentansprüche

1. Verfahren zum Vergleich einer ersten Eigenschaft mit vorgegebenen Eigenschaften eines technischen Systems, a) bei dem mindestens zwei Vergleichsverfahren vorgesehen sind, deren jedes einen Vergleich der ersten Eigenschaft mit den vorgegebenen Eigenschaften des technischen Systems durchführen kann; b) bei dem die mindestens zwei Vergleichsverfahren in einer vorgegebenen Reihenfolge solange abgearbeitet werden, bis ein Ergebnis des Vergleichs bestimmt wird.

2. Verfahren nach Anspruch 1, bei dem das Ergebnis des Vergleichs eine Gleichheit oder eine Verschiedenheit der ersten Eigenschaft von den Eigenschaften des technischen Systems ist.

3. Verfahren nach Anspruch 2, bei dem anhand der Gleichheit die erste Eigenschaft durch das technische System verifiziert wird.

4. Verfahren nach einem der vorhergehenden Ansprüche, bei dem die mindestens zwei Vergleichsverfahren insbesondere aus den folgenden Vergleichsverfahren bestimmt werden: a) SAT-Vergleichsverfahren; b) Simulationsverfahren; c) BDD-Verfahren; d) ATPG-Verfahren; e) Verfahren basierend auf internen Äquivalenzpunkten.

5. Verfahren nach Anspruch 4, bei dem das BDD-Verfahren insbesondere ein ROBDD- Verfahren ist.

6. Verfahren nach Anspruch 5, bei dem das ROBDD-Verfahren bezüglich Blätter oder bezüglich Schnittebenen durchgeführt wird.

7. Verfahren nach einem der vorhergehenden Ansprüche, bei dem das technische System eine Schaltung, insbesondere eine elektrische Schaltung, ist.

8. Verfahren nach einem der vorhergehenden Ansprüche, bei dem das technische System als ein endlicher Automat dargestellt wird.

9. Verfahren nach einem der vorhergehenden Ansprüche, bei dem die erste Eigenschaft als eine Boolesche Funktion dargestellt wird.

10. Verfahren nach einem der vorhergehenden Ansprüche, bei dem durch die erste Eigenschaft ein Verhalten des technischen Systems über einem vorgegebenen Zeitintervall beschrieben wird.

11. Verfahren nach einem der vorhergehenden Ansprüche, bei dem für jedes Verlgeichsverfahren ein Schwellwert für bereitzustellende Ressourcen und/oder zur Verfügung gestellte Zeit bestimmt wird, wobei durch eine Überschreitung des Schwellwerts das jeweilige Vergleichsverfahren als nicht erfolgreich beendet wird.

12. Verfahren nach einem der vorhergehenden Ansprüche, bei dem die Reihenfolge der durchzuführenden

Vergleichsverfahren angepaßt wird, indem dasjenige Vergleichsverfahren zuerst aufgerufen wird, durch das die meisten Vergleiche gelöst werden konnten.

13. Verfahren nach einem der vorhergehenden Ansprüche, bei dem anhand des Ergebnisses des Vergleichs ein Entwurf, eine Anpassung oder eine Steuerung zumindest eines technischen Systems durchgeführt wird.

14. Verfahren nach einem der vorhergehenden Ansprüche, bei dem durch Seiteneffekte bereits aufgerufener Vergleichsverfahren der Vergleich vereinfacht wird.

15. Anordnung zum Vergleich einer ersten Eigenschaft mit vorgegebenen Eigenschaften eines technischen Systems, mit einer Prozessoreinheit, die derart eingerichtet ist, daß a) mindestens zwei Vergleichsverfahren vorgesehen sind, deren jedes einen Vergleich der ersten Eigenschaft mit den vorgegebenen Eigenschaften des technischen Systems durchführen kann; b) die mindestens zwei Vergleichsverfahren in einer vorgegebenen Reihenfolge solange abgearbeitet werden, bis ein Ergebnis des Vergleichs bestimmbar ist.