Vor Ort
Merkzettel Warenkorb
Produktbild: Verifikation digitaler Systeme

Verifikation digitaler Systeme Eine Einführung in den Entwurf korrekter digitaler Systeme

Aus der Reihe Leitfäden und Monographien der Informatik

51,90 €

inkl. gesetzl. MwSt., Versandkostenfrei

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

01.10.1991

Abbildungen

XII, mit Abbildung

Verlag

Vieweg & Teubner

Seitenzahl

308

Maße (L/B/H)

24,4/17/1,8 cm

Gewicht

562 g

Auflage

1991

Sprache

Deutsch

ISBN

978-3-519-02249-7

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

01.10.1991

Abbildungen

XII, mit Abbildung

Verlag

Vieweg & Teubner

Seitenzahl

308

Maße (L/B/H)

24,4/17/1,8 cm

Gewicht

562 g

Auflage

1991

Sprache

Deutsch

ISBN

978-3-519-02249-7

Herstelleradresse

Vieweg+Teubner Verlag
Abraham-Lincoln-Straße 46
65189 Wiesbaden
DE

Email: ProductSafety@springernature.com

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)
  • Produktbild: Verifikation digitaler Systeme
  • I: Grundlagen.- 1 Entwurfskorrektheit.- 1.1 Notwendigkeit von Entwurfskorrektheit.- 1.2 Definition von Entwurfskorrektheit.- 1.3 Verfahren für Entwurfskorrektheit.- 1.4 Zusammenfassung.- 2 Begriff der Abstraktionsebene.- 2.1 Standardisierte Modellvorstellungen.- 2.2 Abstraktionsebenen eines Systems.- 2.3 Zum Begriff der Abstraktion.- 2.4 Abstrakte Mehrebenenmodellierung.- 2.5 Abstraktionsebenen und Sichten.- 2.6 Zusammenfassung.- 3 Modellierung von Verhalten.- 3.1 Zeitfunktionen.- 3.2 Zeitalgebren.- 3.3 Klassifizierung zeitlichen Verhaltens.- 3.4 Aggregationskonzepte.- 3.5 Zusammenfassung.- 4 Sprachen der Prädikatenlogik.- 4.1 Einführung.- 4.2 Formale Sprachen der Prädikatenlogik.- 4.3 Substitutionen.- 4.4 Semantik der Prädikatenlogik.- 4.5 Gültigkeit einer Formel.- 4.6 Zusammenfassung.- 5 Formale Systeme der Prädikatenlogik.- 5.1 Schlußregeln.- 5.2 Tautologische Konsequenzen.- 5.3 Entscheidungsverfahren der Aussagenlogik.- 5.4 Schlußregeln für Quantoren.- 5.5 Theorien der Prädikatenlogik.- 5.6 Erweiterungen einer Theorie.- 5.7 Weitere Sprachmittel der Prädikatenlogik.- 5.8 Zusammenfassung.- II: Elementare Verifikationstechniken für Hardwarebeschreibungen.- 6 Hardwarebeschreibungen.- 6.1 Begriff der Axiomatisierung.- 6.2 Theorie eines Verhaltensmodells.- 6.3 Bestandteile einer Hardwarebeschreibung.- 6.4 Wert- und zeitspezifische Axiome.- 6.5 Beschreibungsspezifische Axiome.- 6.6 Korrektheit einer Aussage.- 6.7 Zusammenfassung.- 7 Logikverifikation.- 7.1 Syntax boolescher Terme.- 7.2 Semantik boolescher Terme.- 7.3 Grundaufgaben der Logikverifikation.- 7.4 Darstellungen boolescher Terme.- 7.5 Systeme von Ersetzungsregeln.- 7.6 Entwicklungsverfahren.- 7.7 Transformation in BDD’s/TDG’s.- 7.8 Vektorielle boolesche Ausdrücke.- 7.9 Äquivalenz vektorieller Ausdrücke.- 7.10 Zusammenfassung.- 8 Statische Beschreibungen.- 8.1 Beschaltungen boolescher Terminals.- 8.2 Zeitliche Semantik boolescher Ausdrücke.- 8.3 Erweiterung auf Vektoren.- 8.4 Statisches Verhalten eines Gesamtsystems.- 8.5 Sortierung der Träger.- 8.6 Wired-Or- und Wired-And-Terminals.- 8.7 Tri-State-Terminals.- 8.8 Zusammenfassung.- 9 Transitionale Beschreibungen.- 9.1 Der bedingte Transfer.- 9.2 Mehrere bedingte Transfers.- 9.3 Bedeutung von Ausdrücken.- 9.4 Aussagen über transitionale Beschreibungen.- 9.5 Transitionsrelation.- 9.6 Vorwärtstransformation.- 9.7 Zweites Verfahren der Vorwärtstransformation.- 9.8 Rückwärtstransformation.- 9.9 Zweites Verfahren der Rückwärtstransformation.- 9.10 Symbolisches Model-Checking.- 9.11 Induktion im Zeitbereich.- 9.12 Erweiterung auf Vektoren.- 9.13 Zusammenfassung.- 10 Kombiniert statisch/transitionale Beschreibungen.- 10.1 srt-Beschreibungen.- 10.2 Bestimmung der Transitionsfunktionen.- 10.3 Zusammenfassung.- 11 Beschreibungen mit Vielfach-Verzögerungen.- 11.1 Einführung.- 11.2 Funktionen zum Erkennen von Flanken.- 11.3 Stabilitätsfunktion.- 11.4 Verzögerungsfunktion.- 11.5 d-statische Beschreibungen.- 11.6 Verschmelzen mehrerer Stabilitätsanforderungen.- 11.7 Setup- und Haltezeit-Bedingungen.- 11.8 Beschreibung eines D-Flipflops.- 11.9 Kombination d-statisch/quasi-transitional.- 11.10 Die ?-Funktion.- 11.11 Zeitlicher Mindestabstand.- 11.12 Aussagen über die absolute Zeit.- 11.13 Zusammenfassung.- 12 Switch-Level Beschreibungen.- 12.1 MOS-Transistoren als Schalter.- 12.2 Grundaufgaben der Switch-Level-Analyse.- 12.3 Der Typ mv.- 12.4 mv-Terme.- 12.5 Modellierung von MOS-Transistoren.- 12.6 Das assumes-Prädikat.- 12.7 Analyse von MOS-Transistor-Netzen.- 12.8 Degradierungseffekte.- 12.9 Zusammenfassung.- 13 Strukturbeschreibungen.- 13.1 Schablonen und Instanzen.- 13.2 Theorie einer Instanz.- 13.3 Regeln für die Verwendung von Ports.- 13.4 Axiome einer Beschreibung mit Instanzen.- 13.5 Verbindungen durch aktuelle Portlisten.- 13.6 Zusicherungen.- 13.7 Zusammenfassung.- III: Entwurfsmethodik.- 14 Strukturierte Entwurfsmethoden.- 14.1 Definition.- 14.2 Mehrebenenverifikation.- 14.3 Verifikation von Teilen.- 14.4 Verifikationsfreundlicher Entwurf.- 14.5 Zusammenfassung.- 15 Erweiterungen von Beschreibungen.- 15.1 Hardware-Spezifikationstechnik.- 15.2 Erweiterung einer Beschreibung.- 15.3 Logikverifikation.- 15.4 Verifikation von ert/srt-Beschreibungen.- 15.5 Zwei-Phasentakt-Systeme.- 15.6 Zusammenfassung.- 16 Interpretierbare Beschreibungen.- 16.1 Begriff der Interpretierbarkeit.- 16.2 Abstraktion im Zeitbereich.- 16.3 Abstraktion im Wertbereich.- 16.4 Arten der Interpretierbarkeit.- 16.5 Zusammenfassung.- 17 Zeitliche Abstraktion.- 17.1 Zeitliche Abstraktion durch Abtasten.- 17.2 Korrespondierende Funktionen und Prädikate.- 17.3 Abstraktion vs. Idealisierung.- 17.4 Zusammenfassung.- 18 Äquivalenz von Beschreibungen.- 18.1 Trägeräquivalenz.- 18.2 Ein/Ausgangs-Äquivalenz.- 18.3 Zusammenfassung.- 19 Verifikation von Teilen.- 19.1 Problemstellung.- 19.2 Kompositionsproblem.- 19.3 Konservative Einbettungen.- 19.4 Struktur-Konsistenz.- 19.5 Einfacher Fall der Komposition.- 19.6 Implementierungsalternativen.- 19.7 Zusammenfassung.- 20 Horizontale Verifikation.- 20.1 Horizontale Verifikation.- 20.2 Transiente und permanente Zusicherungen.- 20.3 Anpassung von Aggregationskonzepten.- 20.4 Reduktion vertikaler auf horizontale Verifikation.- 20.5 Zusammenfassung.- 21 Timing-Verifikation.- 21.1 Grundaufgabe der Timing-Verifikation.- 21.2 Transformations-Strategien.- 21.3 Beispiel einer Transformation.- 21.4 Zusammenfassung.- 22 Struktur von Verifikations-Werkzeugen.- Anhang: Beschreibung eines Divisionswerks auf vier Abstraktionsebenen.