Titlebook: Digitale Hardware/Software-Systeme; Spezifikation und Ve Christian Haubelt,Jürgen Teich Textbook 2010 Springer-Verlag Berlin Heidelberg 201

柔声地说

ALIAS

我要沮丧

Verifikation,re im Bereich eingebetteter Systeme, Implementierungen diversen Optimierungen unterworfen werden. Dies kann einerseits auch manuelle und somit fehleranfällige Verfeinerungen einschließen. Andererseits sind Synthesewerkzeuge typischerweise selbst nicht verifiziert, was bedeutet, dass nicht sichergest

无脊椎

,Äquivalenzprüfung,e Funktion reprÄsentieren (siehe Abb. 4.1). Hierbei kann eine Prüfung zwischen zwei Beschreibungen auf der selben oder unterschiedlichen Abstraktionsebenen erfolgen. Obwohl auf vielen Abstraktionsebenen die Synthese mittlerweile automatisiert ablÄuft [426], ist eine Äquivalenzprüfung hÄufig notwendi

obnoxious

,Eigenschaftsprüfung,r Prüfung funktionaler Eigenschaften wird das Strukturmodell der Implementierung dahin gehend überprüft, ob dieses alle funktionalen Anforderungen erfüllt. Dabei werden typischerweise Gefahrlosigkeits- und Lebendigkeitseigenschaften geprüft. Eine Gefahrlosigkeitseigenschaft besagt, dass nie etwas Sc

propose

Hardware-Verifikation,erschiedenenAbstraktionsebenen. In Abb. 6.1 sind die hier betrachtetenAbstraktionsebenen hervorgehoben. Zunächst werden Methoden zur Äquivalenzprüfung von kombinatorischen und sequentiellen Schaltungen beschrieben, die überwiegend auf der Logikebene eingesetzt werden. Anschließend werden Methoden zu

Free-Radical

Software-Verifikation,räsentiert. Dabei wird die Verifikation sowohl von Assembler- als auch von CProgrammen, die typischen Einschränkungen für eingebettete Software unterliegen, betrachtet. Danach werden Verfahren zur Testfallgenerierung für simulative Verifikationsmethoden für Software zusammen mit den zugehörigen über

miscreant

统治人类

Digitale Hardware/Software-Systeme978-3-642-05356-6Series ISSN 1614-5216

Insul岛

Singende Gesellschaft – Bestandsaufnahmere im Bereich eingebetteter Systeme, Implementierungen diversen Optimierungen unterworfen werden. Dies kann einerseits auch manuelle und somit fehleranfällige Verfeinerungen einschließen. Andererseits sind Synthesewerkzeuge typischerweise selbst nicht verifiziert, was bedeutet, dass nicht sichergestellt ist, dass das Syntheseergebnis korrekt ist.