Matthias Bernauer - Freiburg im Breisgau
      Start > Skript-Sammlung > Rechnerarchitektur > Modellpruefung - CTL-Operatoren - Hardwa... >>







Modellpruefung - CTL-Operatoren - Hardwaresynthese



  • Modellprüfung: erfüllt eine Schaltung bestimmte (sequentielle) Eigenschaften
    Was ist eine Modellprüfung? Die Frage, ob ein Schaltwerk eine gegebene Spezifikation erfüllt?
    - Modellierung des Schaltwerkes durch endliche Automaten
    - Spezifikation der Eigenschaften in temporalen Aussagenlogiken
    - Model Checking: Fixpunktiteration, Traversierung des Zustandsraumes, BDDs [vollständig]
    - Bounded Model Checking: SAT-Solver zur Lösung
    [unvollst.: nur zum finden von Fehlern kein Korrektheitsbeweis!]
    >> Temporale Aussagenlogiken (CTL*, CTL, LTL)
    Formeln in temporalen Aussagelogiken beschreiben gewünschte Eigenschaften des Designs.
    Formeln werden rekursiv aufgebaut auf Basis von
    - atomaren Formeln: Signale des Designs, z.B.: yi bedeutet: Ausgang yi hat aktuell den Wert 1
    - Booleschen Operatoren, z.B. ¬φ, φ ∧ ψ, φ ∨ ψ, z.B.: yi ∧ yj
    - temporalen Operatoren: machen Aussagen über
    einen einzelnen Berechnungspfad des Berech-
    nungsbaumes des zugehörigen Schaltwerkes
    z.B. Gϕ oder always: Formel ϕ gilt in jedem
    Zustand des
    Pfades.


    z.B. Fϕ oder sometimes: Formel ϕ gilt in einem Zustand des Pfades.
    z.B. Xϕ oder next: Formel ϕ gilt für den Pfad beginnend mit dem
    nächsten, d.h. zweiten Zustand des Pfades
    z.B. ϕUψ oder until: Formel ϕ solange bis Formel ψ gilt

    Diese vier Operatoren machen Aussagen über Berechnungspfade

    Aussagenlogiken mit temporalen Operatoren
    - machen Aussagen über Eigenschaften von Zuständen auf der Basis von Pfadformeln ϕ:
    - Aϕ oder for all paths: Formel ϕ gilt auf allen möglichen Berechnungspfaden, die in dem
    Zustand beginnen.
    - Eϕ oder there exists a path: Formel ϕ gilt auf einem Berechnungspfad, der in dem Zustand
    beginnt.
    Jede Zustandsformel kann im folgenden Sinne als Pfadformel interpretiert werden:
    Wenn die Zustandsformel ϕ in einem Zustand gilt, dann gilt sie für jeden Pfad, in dessen Anfangszustand die Zustandsfolgel ϕ gilt

    Welche typischen Eigenschaften besitzt die LTL?
    Sicherheit: a und b werden nie gleichzeitig war: G not(a oder b)
    Lebendigkeit: Jede Anforderung wird innerhalb von 5 bis 7 bestötigt: G(req->F[5,7]ack)
    Fairness: Innerhalb von 30 Schritten gilt mindestens einmal a: G F[30]a
    Warum ist es nicht sinnvoll die Korrektheit einer Schaltung über Signalabfolgen zu testen?
    Weil es davon unendlich viele gibt, das Problem dadurch semi.entscheidbar wird, deshalb löst man das an einem formalen Modell, einem endlichen Automaten

  • Theorembeweisen: interaktive Methode, basierend auf Logik höherer Ordnung
    (Logik höherer Ordnung unentscheidbar)
    - Modellierung der Schaltung/Eigenschaften in Logik höherer Ordnung
    - interaktiver Beweis durch Anwendung von Theoremen
    - oft kombiniert mit Heuristiken zur Automation des Beweises oder automatischen Entscheidungsprozeduren
    Was ist Theorembeweisen? Man modelliert die Schaltung und deren Eigenschaften in einer Logik höherer Ordnung und beweist die interaktiv durch die jeweiligen Theorem der Logik. Kombinieren kann man dies mit diversen Heuristiken zur Automation des Beweises und durch automatische Ent.-proz.
    Was wird bei der Timinganalyse bestimmt? [Wie hoch man die Schaltung takten kann]

      1. Hardwaresynthese
        Automatische Abbildung von Beschreibungen auf hohen Abstraktionsebenen in niedrige Ebenen
        - Highlevel-Synthese
        Algorithmische Ebene ⇒ Registertransfer Ebene
        - Allokation
        Auswahl der HW-Komponenten für die Operationen
        - Ablaufplanung (Scheduling)
        Bestimmung der Zeitpunkte, an denen die
        Operationen auszuführen sind
        - Bindung
        Zuordnung von Variablen zu Registern, Operationen zu funktionalen Einheiten und
        Kommunikationskanälen zu Bussen
        - Gattersynthese
        Registertransfer Ebene ⇒ Gatterebene
        - Technologieabbildung
        Gatterebene ⇒ Transistorebene

Google MSN Suche
<< Start | Studium | Poolmgr | Tanzen | GPG | Impressum >>
Matthias Bernauer