Der Anstieg der Soft-Error-Rate (SER) reduziert zunehmend die Zuverlässigkeit heutiger Schaltkreise, so dass fehlertolerante Systeme implementiert werden. Diese Fehlertoleranz bzw. Robustheit einer Implementierung muss verifiziert werden. Hier wird ein formaler Ansatz vorgestellt, der dieses Verifikationsproblem in Teilprobleme zerlegt. Die Experimente zeigen einen deutlichen Anstieg der Effektivität des neuen Verfahrens gegenüber einem monolithischen Ansatz. Fehlertolerante Implementierungen von Systemen gewinnen zunehmend an Bedeutung. Deshalb werden Designwerkzeuge benöigt, die die Implementierung auf Korrektheit bzw. den Grad der Fehlertoleranz analysieren. Dazu wurden bereits simulations-basierte und formale Methoden vorgestellt. Nur formale Methoden ermöglichen eine vollständige Analyse, da sie alle möglichen Eingangsbelegungen betrachten. Die genannten formalen Ansätze betrachten das ganze System als ein monolithisches Modell. Jedoch geraten damit formale Methoden an ihre Grenzen, wenn es darum geht, Systeme mit einer großen Anzahl an Komponenten zu analysieren. Für die formale Eigenschaftsprüfung wurden bereits Techniken, wie z.B. Dekomposition und Abstraktion zur Steigerung der Effektivität eingesetzt. Jedoch wurden diese für die formale Robustheitsprüfung bisher nicht betrachtet. In dieser Arbeit wird Dekomposition zur Steigerung der Effektivität der formalen Robustheitsprüfung eingesetzt. Dazu wird der zu analysierende Schaltkreis zunächst in Teilschaltkreise zerlegt und basierend auf dem Robustheitsmodell aus untersucht. Der Anstieg der Soft-Error-Rate (SER) reduziert zunehmend die Zuverlässigkeit heutiger Schaltkreise, so dass fehlertolerante Systeme implementiert werden. Diese Fehlertoleranz bzw. Robustheit einer Implementierung muss verifiziert werden. Hier wird ein formaler Ansatz vorgestellt, der dieses Verifikationsproblem in Teilprobleme zerlegt. Die Experimente zeigen einen deutlichen Anstieg der Effektivität des neuen Verfahrens gegenüber einem monolithischen Ansatz. Im folgenden wird der im Beitrag vorgestellte Ansatz experimentell evaluiert. Es werden partiell redundant ausgelegte Schaltkreise aus der ISCAS'85 Benchmarks-Suite und eine Arithmetic Logic Unit (ALU) mit 8- bzw. 16-bit-Datenpfad betrachtet. Die funktionalen Einheiten der ALU werden durch eine Modulo-Prüfung auf Fehlfunktionen geprüft. Ergebnisse sind in Tabelle I aufgelistet. Beim kompositionellem Ansatz wurde eine SAT-basierte Approximation der Propagation verwendet. Als SAT-Beweiser wurde MiniSAT mit einer Erweiterung zum inkrementellen Lösen verwendet. Die ersten drei Spalten geben Details über den Schaltkreis an, wie Name, Größe (C) und Anzahl der betrachteten Teilschaltkreise (TS). Für beide Verfahren sind die berechnete Robustheit R(C) und die Laufzeit in CPU-Sekunden angegeben. Das kompositionelle Verfahren liefert eine untere Schranke der Robustheit (Rlb(C)), da bezüglich der Propagation ein optimistischer approximativer Ansatz genutzt wurde. Die kleineren Schaltkreise c5315-red und ALU-8 können von beiden Verfahren vollständig klassifiziert werden. Allerdings ist die Laufzeit für den kompositionellen Ansatz deutlich geringer. Der berechnete Wert für die Robustheit liegt im Falle von c5315-red deutlich unterhalb des tatsächlichen Wertes, da oft optimistisch angenommen wird, dass Fehlerwerte propagiert werden können, obwohl dies nicht der Fall ist. Bei der ALU ist die Propagation von Fehlereffekten immer möglich, da gut sensitivierbare funktionale Blöcke als Teilschaltkreise betrachtet wurden. Demzufolge ist Rlb(C) identisch mit R(C). Die größeren Schaltkreise können vom monolithischen Verfahren nicht innerhalb von 5000s abschließend klassifiziert werden. Für c7552-red werden einige Komponenten aber innerhalb der Laufzeit als nicht robust klassifiziert, so dass sich eine obere Schranke ergibt. Im Falle der ALU kann das monolithische Verfahren nur die 8-Bit-ALU klassifizieren. Das kompositionelle Verfahren kann beide Schaltkreise behandeln. Die 16-Bit-ALU wird lediglich der Teilschaltkreis, der die Multiplikation realisiert, nicht klassifiziert (durch a gekennzeichnet). Alle anderen Komponenten können klassifiziert werden. Insgesamt kann durch das kompositionelle Verfahren die Effizienz deutlich gesteigert werden. Insbesondere werden Schaltkreise, die keine monolithische Behandlung erlauben, handhabbar. In Zukunft soll untersucht werden, wie der formale Ansatz von einer existierenden Testbench profitieren kann, die Sequenzen vorgibt, um Teile eines komplexen Schaltkreises zu prüfen bzw. zu sensitivieren.
The increase of the Soft-Error-Rate (SER) reduces the reliability of today's circuits. Thus, fault tolerant systems are implemented. The fault tolerance and robustness of an implementation have to be verifed. Here we propose a formal approach which decomposes the verification problem into smaller problems. Experiments show a significant increase of the effectiveness of the new approach against a monolithic approach.
Kompositionelle Formale Robustheitsprüfung
2010
2 Seiten, 1 Tabelle, 6 Quellen
Conference paper
German
TIBKAT | 1977
|Absicherung sicherheitskritischer Systeme - formale Verifikation
Automotive engineering | 2009
|Formale Techniken für die Eisenbahnsicherungstechnik
IuD Bahn | 1999
|Formale Techniken fur die Eisenbahnsicherungstechnik
British Library Conference Proceedings | 2000
|Formale Sicherheitsanalyse einer funkbasierten Bahnübergangssteuerung
Tema Archive | 2000
|