#+title: Verifikation digitaler Systeme
#+author: Florian Guthmann
#+email: florian.guthmann@fau.de
#+language: de
#+options: num:nil \n:t html-style:nil html5-fancy:t html-postamble:nil
#+html_doctype: xhtml5
#+html_head:
#+html_head:
#+html_mathjax: path:/~oc45ujef/mathjax/es5/tex-mml-chtml.js
#+begin_comment
Fehler im Skript:
- Kapitel 2, S.13: verbogen -> verborgen, Verhaltensabstration -> Verhaltensabstraktion
- Kapitel 3.1, S.9: (pedant) Bei Definition von δ+ und λ+ sollte ":=" verwendet werden
- Kapitel 3.1, S,28: (pedant) wieder ":=" und evtl ein $a \in I$ hinzufügen
#+end_comment
* Grundlagen
#+caption: Doppeldachmodell
#+attr_html: :class center-image
[[./img/dach.png]]
** BDDs
#+attr_html: :border 2 :rules all :frame border
| Zerlegung | | low child | high child |
|----------------+-----------------------------------------------------------------------------------------+--------------------+-------------------------------------------|
| Shannon | $f = x \land f_{\lvert x = 1} \lor (\neg x) \land f_{\lvert x = 0}$ | $f_{\lvert x = 0}$ | $f_{\lvert x = 1}$ |
| positive Davio | $f = f_{\lvert x = 0} \oplus x \land (f_{\lvert x = 1} \oplus f_{\lvert x = 0})$ | $f_{\lvert x = 0}$ | $f_{\lvert x = 1} \oplus f_{\vert x = 0}$ |
| negative Davio | $f = f_{\lvert x = 1} \oplus (\neg x) \land (f_{\lvert x = 1} \oplus f_{\lvert x = 0})$ | $f_{\lvert x = 1}$ | $f_{\lvert x = 1} \oplus f_{\vert x = 0}$ |
* Simulation und Formale Verifikation
** Simulation
- Evalulierung des Entwurfs durch Simulation von Stimuli, funktional oder zufällig gewählt.
- erfasst nicht das gesamte Verhaltensspektrum
- überprüft jeweils genau /einen/ Punkt im Eingaberaum
- durch *Eingabe* getrieben
** Formale Verifikation
- überprüft /Gruppen/ von Punkten im Eingaberaum
- durch *Ausgabe* getrieben
** Steuerbarkeit und Beobachtbarkeit
- Steuerbarkeit :: wie schwierig ist es, einen bestimmten (internen) Zustand in einem System einzustellen.
- Beobachtbarkeit :: wie schwierig ist es, einen bestimmten (internen) Zustand eines Systems zu beobachten.
** Abstraktion
- Strukturelle Abstraktion :: Interne Systemdetails werden verborgen
- Verhaltensabstraktion :: Partielle Spezifikationen, die das Verhalten nicht vollständig beschreiben
- Datenabstraktion :: Werte auf höheren Abstraktionsebenen darstellen ($\mathbb{N}$ statt $\mathbb{B}^n$)
- Zeitabstraktion :: Zeitraster vergröbern (Befehlszyklen statt Taktzyklen)
#+attr_html: :border 2 :rules all :frame border
| Ebene | Verhalten | Struktur | Daten | Zeit |
|-------------+----------------------+------------------------------+----------------+----------------------|
| System | Algorithmen | Prozessoren, Busse, Speicher | Zahlen, Unions | Kausalität |
| Architektur | Mult,Add | ALUs, Multiplizierer | Bitvektoren | Takte |
| Logik | Boolesche Funktionen | Gatter, FlipFlops | Bits | Gatterlaufzeiten |
| Modul | Funktionen | Prozesse, OS-Dienste | Zahlen | Takte |
| Block | Instruktionen | Assemblerbefehle | Bytes | Instruktionsschritte |
* Äquivalenzprüfung
** Automatentheorie
#+begin_definition
Ein /endlicher Zustandsautomat/ (Mealy) $M = (S,E,A, \delta, \lambda, s_0)$.
- $S$ :: endliche Menge von Zuständen
- $E, A$ :: Ein- und Ausgabealphabet
- $\delta : S \times E \to S$ :: Überführungsfunktion
- $\lambda : S \times E \to A$ :: Ausgabefunktion
- $s_0$ :: Startzustand
#+end_definition
*** Sequenzen
- endliche Sequenzen von Eingangssymbolen $w \in E^+$
- erweiterte Überführungsfunktion $\delta^+ : S \times E^+ \to S$
\[
\delta^+ (s,w) := \begin{cases}
\delta(s,w) & \lvert w \rvert = 1\\
\delta(\delta^+(s,w_1 \circ \dots \circ w_{\lvert w \rvert - 1}), w_{\lvert w \rvert}) & \lvert w \rvert > 1
\end{cases}
\]
- erweiterte Ausgabefunktion $\lambda^+ : S \times E^+ \to S$
\[
\lambda^+ (s,w) := \begin{cases}
\lambda(s,w) & \lvert w \rvert = 1\\
\lambda^+(s,w_1 \circ \dots \circ w_{\lvert w \rvert - 1}) \circ \lambda(\delta^+(s,w_1 \circ \dots \circ w_{\lvert w \rvert - 1}), w_{\lvert w \rvert}) & \lvert w \rvert > 1
\end{cases}
\]
*** Erreichbarkeit
Für $T \subset S$ sei
\begin{align*}
\mathrm{REACH}(T) &:= T \cup \{s \in S \mid \exists t \in T, w \in E^+ .\, \delta^+(t,w) = s\}\\
\mathrm{PRED}(T) &:= \{s \in S \mid \exists t \in T, e \in E .\, \delta(s,e) = t\}\\
\mathrm{SUCC}(T) &:= \{s \in S \mid \exists t \in T, e \in E .\, \delta(t,e) = s\}\\
\end{align*}
*** Äquivalenzprüfung
#+begin_definition
Zwei Automaten $M = (S, E, A, \delta, \lambda, s_0)$ und $M' = (S', E, A, \delta', \lambda', s_0')$ heißen /äquivalent/ ($M \equiv M'$) wenn
\[
\forall w \in E^+ .\, \lambda^+(s_0,w) = \lambda'^+(s'_0, w)
\]
#+end_definition
#+begin_definition
Seien $M = (S, E, A, \delta, \lambda, s_0)$ und $M = (S', E, A, \delta', \lambda', s_0')$ zwei Automaten und $s \in S, s' \in S'$ Zustände.
$s$ und $s'$ heißen /zustandsäquivalent/ ($s \sim s'$), wenn
\[
\forall e \in E .\, \lambda(s,e) = \lambda'(s',e) \land \delta(s,e) \sim \delta'(s',e)
\]
#+end_definition
#+begin_theorem
Zwei Automaten $M, M'$ sind genau dann äquivalent, wenn ihre Startzustände äquivalent sind.
\[
((S, E, A, \delta, \lambda, s_0) \equiv (S', E, A, \delta', \lambda', s_0')) \Leftrightarrow s_0 \sim s'_0
\]
#+end_theorem
*** Produktautomaten
Bei der Äquivalenzprüfung müssen nicht alle Kombinationen von Zuständen sondern nur die, in denen die Automaten /zum gleichen Zeitpunkt/ sein können, verglichen werden.
#+begin_definition
Für zwei Automaten $M = (S, E, A, \delta, \lambda, s_0)$ und $M' = (S', E, A, \delta', \lambda', s_0')$ ist der /Produktautomat/ $M_p$ definiert als
\begin{align*}
M_p &:= (S \times S', E, \{0,1\}, \delta_p, \lambda_p, (s_0, s'_0))\\
\delta_p((s,s'), e) &:= (\delta(s,e), \delta'(s',e))\\
\lambda_p((s,s'), e) &:= (\lambda(s,e) =_{\mathbb{B}} \lambda'(s',e))
\end{align*}
#+end_definition
und damit für die *Zustandsäquivalenz*:
\[
s \sim s' \Leftrightarrow \forall e \in E .\, \lambda_p((s,s'), e) = 1 \land \delta_p((s,s'),e) \in \sim
\]
und *Automatenäquivalenz*:
\[
M \equiv M' \Leftrightarrow \forall s \in \mathrm{REACH}(\{(s_0,s'_0)\}), e \in E .\, \lambda_p(s,e) = 1
\]
*** Äquivalenzprüfung durch Fixpunktiteration
**** Forward Traversal
1. Starte mit $S_r \leftarrow \{s_0\}$ und $S_n \rightarrow S_r$
2. Wenn $\exists s \in S_n, e \in E .\, \lambda_p(s,e) = 0$ sind die Automaten nicht äquivalent.
3. Sonst setze $S_n \leftarrow \delta_p(S_n) \setminus S_r$ und $S_r \leftarrow S_r \cup S_n$
Bis $S_n = \emptyset$
**** Backward Traversal
1. Starte mit $S_n \leftarrow \{s \in S \mid \exists e \in E .\, \lambda_p(s,e) = 0\}$ und $S_e \leftarrow S \setminus S_n$
2. Wenn $s_0 \in S_n$ dann sind die Automaten nicht äquivalent
3. Sonst setze $S_n \leftarrow \delta^{-1}(S_n) \cap S_e$ und $S_e \leftarrow S_e \setminus S_n$
Bis $S_n = \emptyset$
** Repräsentation von Funktionen
#+begin_definition
Für eine Menge von Funktionen $F$ heißt $(R,\Phi : R \to F)$ /Repräsentation/ von $F$ und
$r \in R$ repräsentiert $f \in F$, wenn $\Phi(r) = f$.
#+end_definition
Eine Repräsentation $(R, \Phi)$ von $F$ heißt
- /vollständig/, wenn $\Phi$ surjektiv ist
- /eindeutig/, wenn $\Phi$ injektiv ist
- /kanonisch/, wenn $\Phi$ bijektiv ist
Eine Repräsentation ist sinnvoll wenn sie kanonisch ist, da dann Äquivalenz in der Repräsentation und der Funktionsmenge zusammenfallen.
Außerdem sollten
- Operationen wie $\Phi(r) + \Phi(r')$, $\Phi(r) \cdot \Phi(r')$ und $-\Phi(r)$ effizient berechenbar
- Substititionen wie $[\Phi(r')/x]\Phi(r)$ effizient durchführbar
sein
*** Taylorreihen
Für ein Intervall $I$ und eine beliebig oft differenzierbare Funktion $f : I \to \mathbb{R}$ ist
\[
P_f(x) := \sum_{n=0}^{\infty}\frac{f^{(n)}(a)}{n!}\cdot(x - a)^n
\]
die Taylorreihe mit Entwicklungspunkt $a \in I$
*** TODO Taylorentwicklungsdiagramme (TED)
Nehme $f$ als beliebig oft differenzierbar und $a = 0$ an:
\[
f(x) = f(0) + x \cdot f'(0) + \frac{1}{2}\cdot x^2 \cdot f''(0)+\dots
\]
** TODO Symbolisch
Die binäre Kodierung einer Menge $E$ ist gegeben durch
\[
\sigma_E : E \to \mathbb{B}^n, \text{mit } n \geq \log_2(\lvert E \rvert)
\]
#+begin_definition
Eine /boolesche/ Funktion ist eine Abbildung $f : \mathbb{B}^n \to \mathbb{B}$.
#+end_definition
z.B
#+attr_html: :border 2 :rules all :frame border
| $x_1$ | $x_2$ | $x_3$ | $f(x_1,x_2,x_3)$ |
|-------+-------+-------+------------------|
| 0 | 0 | 0 | 0 |
| 0 | 0 | 1 | 1 |
| 0 | 1 | 0 | 1 |
| 0 | 1 | 1 | 0 |
| 1 | 0 | 0 | 1 |
| 1 | 0 | 1 | 1 |
| 1 | 1 | 0 | 1 |
| 1 | 1 | 1 | 1 |
#+begin_definition
- Eine /Bewertung/ ist eine Abbildung $V \to \mathbb{B}$, wobei $V$ die Menge der Variablen darstellt.
- Eine Boolesche Funktion $f$ heißt /gültig/, wenn sie für alle Bewertungen wahr ist
- Eine Boolesche Funktion $f$ heißt /erfüllbar/, wenn eine wahre Bewertung existiert
#+end_definition
** Strukturell
Beweise Äquivalenz von System 1 und System 2 durch
- Äquivalenzbeweis von Subsystem 1.1 und 2.1
- Äquivalenzbeweis von Subsystem 1.2 und 2.2
Probleme stellen dabei *False Negatives* z.B
Aus System 1 \sim System 2 und Subssystem 1.1 \sim 2.1 folgt *nicht*, dass Subsystem 1.2 \sim Subsystem 2.2
Da an den Schnittpunkten nicht alle Wertebelegungen einstellbar sein müssen.
Daher:
- teurer Erfüllbarkeitstest an den Schnittpunkten
- don't-care-Bedingungen
- mehrere überlappende Schichten auf Äquivalenz prüfen
*** OFDDs
#+begin_definition
Die /positive Davio-Dekomposition/ einer booleschen Funktion $f$:
\[
f(x_1,\dots,x_n) = f_{\lvert x = 0} \oplus x_i \land (f{\lvert x = 1} \oplus f{\lvert x = 0})
\]
#+end_definition
* Temporale Aussagenlogik
#+begin_definition
Eine /temporale Struktur/ $M = (S,R,L)$ über einer Menge atomarer Formeln $V$ besteht aus
- einer Menge von Zuständen $S$
- einer linkstotalen Übergangsrelation $R \subset S \times S$
- einer Markierungsfunktion $L : S \to \mathcal{P}(V)$
#+end_definition
#+begin_definition
Ein /Pfad/ in einer temporalen Struktur $M$ ist eine unendliche Folge $s = (s_0,s_1,\dots)$ von Zuständen mit
\[
\forall i \in \mathbb{N} .\, (s_i, s_{i + 1}) \in R
\]
Der /Suffix/ $s^{(j)}$ eines Pfades $s$ ist $s^{(j)} = (s_j, s_{j+1},\dots)$
#+end_definition
** Linear Time Logic (LTL)
Hier gibt es keine Verzweigungen in der temporalen Struktur, d.h. es existiert genau ein Pfad.
#+attr_html: :border 2 :rules all :frame border
| Temporaler Operator | | Bedeutung |
|------------------------+------------+---------------------------------------------------------------------------|
| $\mathrm{X} \Psi$ | /next/ | $\Psi$ gilt im nächsten Zustand |
| $\mathrm{F} \Psi$ | /finally/ | $\Psi$ gilt in einem Zustand |
| $\mathrm{G} \Psi$ | /globally/ | $\Psi$ gilt in jedem Zustand |
| $\Phi \mathrm{U} \Psi$ | /until/ | $\Phi$ gilt bis zu einem Zustand (der existieren muss) in dem $\Psi$ gilt |
| $\Phi \mathrm{R} \Psi$ | /release/ | $\Psi$ gilt solange, bis auch $\Phi$ gilt |
** Computation Tree Logic (CTL)
Erweitert *LTL* mit Verzweigungen in der temporalen Struktur und Quantoren:
#+attr_html: :border 2 :rules all :frame border
| Pfadquantor | Bedeutung |
|------------------+------------------------------------------|
| $\mathrm{E}\Psi$ | Es existiert ein Pfad in dem $\Psi$ gilt |
| $\mathrm{A}\Psi$ | $\Psi$ gilt für alle Pfade |
Einem LTL-Operator in $\Psi$ muss immer ein Pfadquantor vorangestellt werden, um eine valide CTL-Formel zu erhalten.
$\Psi$ muss außerdem quantorenfrei sein ($\mathrm{AFAG} \Phi$ ist also keine CTL-Formel!).
Somit ergeben sich acht Grundoperatoren mit Basis $\{\mathrm{EX}, \mathrm{EG}, \mathrm{EU}\}$:
\begin{align*}
\mathrm{AX}\Phi &\Leftrightarrow \neg\mathrm{EX}(\neg\Phi)\\
\mathrm{AG}\Phi &\Leftrightarrow \neg\mathrm{EF}(\neg\Phi)\\
\mathrm{AF}\Phi &\Leftrightarrow \neg\mathrm{EG}(\neg\Phi)\\
\mathrm{EF}\Phi &\Leftrightarrow \mathrm{E}(\mathrm{true}\mathrm{U}\Phi)\\
\end{align*}
** CTL*
Nicht alle LTL-Formeln lassen sich in CTL ausdrücken, und umgekehrt.
#+attr_html: :border 2 :rules all :frame border
| Formel | LTL | CTL | CTL* |
|------------------------------------------+-----+-----+------|
| $\mathrm{AFG}\Psi$ | ✅ | ❌ | ✅ |
| $\mathrm{EX}\Psi$ | ❌ | ✅ | ✅ |
| $\mathrm{AG}\Psi$ | ✅ | ✅ | ✅ |
| $\mathrm{EX}\Psi \land \mathrm{AFG}\Psi$ | ❌ | ❌ | ✅ |
CTL* übernimmt die temporalen Operatoren von *CTL*, es muss aber kein Pfadquantor direkt vorangestellt werden und Pfadquantoren dürfen geschachtelt werden.
CTL* ist also ein Superset von *CTL* und *LTL* (wobei LTL-Formel implizit $\mathrm{A}$ -quantifiziert werden).
* TODO Formale Eigenschaftsprüfung
Sei $M = (S,R,L)$ ein endlicher Automat als temporale Struktur mit
- $S$ Menge der Zustände
- $R \subset S \times S$ Übergangsrelation
- $L : S \to \mathcal{P}(V)$ die Label-Funktion
Systemeigenschaften sind {LTL,CTL,CTL*}-Formeln
Identfiziere im Folgenden:
- CTL-Formel $\Phi$ mit der Menge der Zustände $S_\Phi \subseteq S$ in denen $\Phi$ gilt
- $\Phi \land \Psi$ mit $S_\Phi \cap S_Psi$ und $\Phi \lor \Psi$ mit $S_\Phi \cup S_\Psi$
- $\neg\Phi$ mit $S \setminus S_\Phi$
- $\mathtt{true}$ mit $S$ und $\mathtt{false}$ mit $\emptyset$
#+begin_definition
Sei $\Phi$ eine Formel und $y$ eine Variable in $\Phi$.
Dann ist $\tau = \lambda y.\, \Phi$ ein /Funktional/.
Eine Formel $p$ heißt /Fixpunkt/ eines Funktionals $\tau$, wenn $\tau(p) = p$
Ein Funktional $\tau$ heißt /monoton/, wenn $p \subset q \implies \tau(p) \subset \tau(q)$
Für ein monotones Funktional $\tau := \lambda y .\, \Phi$ existiert der /kleinste Fixpunkt/
\[
\mu y.\, \Phi
\]
als Schnitt aller Fixpunkte von $\tau$
Für ein monotones Funktional $\tau := \lambda y .\, \Phi$ existiert der /größte Fixpunkt/
\[
\nu y.\, \Phi
\]
als Vereinigung aller Fixpunkte von $\tau$
#+end_definition
#+begin_theorem
Sei $\tau = \lambda y.\, \Phi$ ein monotones Funktional und $\Phi$ eine CTL-Formel, dann
\begin{align*}
\mu y.\, \Phi &= \bigcup_i \tau^i(\mathrm{false})\\
\nu y.\, \Phi &= \bigcap_i \tau^i(true)
\end{align*}
Wobei $\tau^i$ die $i$ -fache Komposition von $tau$ mit sich selbst ist ($\tau^0(p) = p$)
#+end_theorem
Für CTL-Formel gilt:
\begin{align*}
\mathrm{EF}\,p &= \mu y.\, (p \lor \mathrm{EX}\, y)\\
\mathrm{EG}\,p &= \nu y.\, (p \land \mathrm{EX}\, y)\\
\mathrm{E}(p \,\mathrm{U}\,q) &= \mu y.\, (q \lor (p \land \mathrm{EX}\, y))\\
\end{align*}
** TODO Symbolic Model Checking
** Bounded Model Checking
Grundidee: Restriktiere auf Pfade der Länge $k$, falte auf und reduziere auf SAT.
* Simulationsbasierte Eigenschaftsprüfung
** Assertions
- statisch :: "zero-time"-Bedingungen die funktionale Korrektheit garantieren
- temporal :: garantieren funktionale Korrektheit über eine Zeitperiode
** Überdeckung
- Code-Überdeckung :: auf einer konkreten Entwurfssprache
- Anweisungsüberdeckung :: Anteil der durchlaufenden Statements
- Grundblocküberdeckung :: Anteil der durchlaufenden Blöcke (Statements zu feingranular)
- Pfadüberdeckung :: Anteil der durchlaufenden Pfade
- Zweigüberdeckung :: Anteil der durchlaufenden Zweige (nicht äquivalent zu Pfaden!)
- Funktionale Überdeckung :: auf einem formalen Modell
- Parameterüberdeckung :: Entwurfssprache oder formales Modell
* Softwareverifikation
** Uninterpretierte Funktionen
Um von der Funktionalität zu abstrahieren wird nur Kongruenz gefordert:
\[
a = b \implies f(a) = f(b)
\]
\begin{align*}
\mathtt{msm\, dx, a0, a1} \quad& \mathtt{dx} := f_{\mathrm{add}}(\mathtt{dx}^*, f_{\mathrm{mult}}(\mathtt{a0}^*, \mathtt{a1}^*)\\
\end{align*}
z.B. Äquivalenz zweier C-Programme
#+begin_src c
a1 = b1 + c1;
#+end_src
#+begin_src c
tmpB2 = b2;
tmpC2 = c2;
a2 = tmpB2 + tmpC2;
#+end_src
Es ergeben sich schrittweise die Äquivalenzklassen:
\begin{align*}
E_1 &:= \{\mathtt{b1},\mathtt{b2},\mathtt{tmpB2}\}\\
E_2 &:= \{\mathtt{c1},\mathtt{c2},\mathtt{tmpC2}\}\\
E_3 &:= \{\mathtt{a1},\mathtt{tmpB2} + \mathtt{tmpC2}\}\\
E_4 &:= \{\mathtt{a2},\mathtt{tmpB2} + \mathtt{tmpC2}\}\\
E_3 &:= \{\mathtt{a1}, \mathtt{a2},\mathtt{tmpB2} + \mathtt{tmpC2}\}
\end{align*}
*** Falschnegative Ergebnisse
Hier entstehen falschnegative Ergebnisse, da z.B. $f_{\mathrm{mult}}(a,b) = f_{\mathrm{mult}}(b,a)$ nicht herleitbar ist.
Entsprechend werden die nötigen Axiome hinzugefügt.
*** Falschpositive Ergebnisse
Es wird von konkreten Datentypen abstrahiert (z.B $\mathbb{R}$ statt =Float=).
Insbesondere gilt in =Float= die Identität $(x+y) - z = (x - z) + y$ *nicht*
Die entsprechenden Datentypen müssen also hinzugefügt werden.
** PDG
Symbolische Simulation skaliert schlecht für größere Programme.
Deshalb interessante Stellen (Verifikationsbereiche) mittels *PDG* wählen.
#+begin_definition
Ein Program Dependency Graph ist ein bipartiter Graph $(V_P \uplus V_Z, E_C \uplus E_D)$ wobei
- $V_P$ Prädikate von kond. Sprüngen
- $V_Z$ Zuweisungen
- $E_C$ Kontrollfluss
- $E_D$ Datenabhängigkeiten
darstellen
#+end_definition
** Statische Analyse
- Konkrete Interpretation :: führe Programm aus und teste Wertebereich
- Abstrakte Interpretation :: teste Wertebereiche
- Vorzeichen-Wertebereich :: =pos,neg,zero=
- Kongruenz-Wertebereich :: $x \bmod k$ für $k \in \mathbb{N}$
- Intervall-Wertebereich :: $\{[a,b] \mid a \leq b, a,b \in \mathbb{Z}\}$
*** Hoare-Logik
siehe SemProg
** Zeitanalyse
- Core Execution Time :: Ausführungszeit ohne Unterbrechungen
- Best Case Execution Time (BCET) :: Bestmögliche Ausführungszeit
- Worst Case Execution Time (WCET) :: Schlechtestmögliche Ausführungszeit
Die Analyse kann in zwei (nicht unabhängige) Teilprobleme zerlegt werden:
- Programmpfadanalyse :: welche Ausführungspfade führen zur schnellsten/langsamsten Ausführung
- Modellierung der Zielarchitektur :: Architekturmerkmale wie Caches, Pipelining usw.
Hierbei gibt es die Möglichkeiten:
- Instruction Time Addition :: Annahme: jede Instruktion hat konstante Ausführungszeit
- Path Segment Simulation :: zyklenakurate Modellierung
*** Echtzeitscheduling
#+begin_definition
Ein /Task-Graph/ ist ein Tupel $G = (V,E)$ mit
- $V$ Menge der Tasks
- $E \subset V \times V$ Menge der Task-abhängigkeiten
- $t_d : V \to \mathbb{R} \cup \{\infty\}$ ordnet jedem Task eine /Deadline/ zu
- $\Delta t : V \to \mathbb{R}$ ordnet jedem Task eine Ausführungsdauer zu
#+end_definition
#+begin_definition
Für einen /Ablaufplan/
- $t_s,t_e : V \to \mathbb{R}$ ordnen jedem Task Start- und Endzeitpunkt zu
- $t_L(v) := t_e(v) - t_d(v)$ ordnet jedem Task seine /Lateness/ (d.h Abweichung des Endzeitpunkts von der Deadline) zu
#+end_definition
**** Earliest-due-date (EDD)
Sortiere Task aufsteigend nach Deadlines.
Erzeugt einen Ablaufplan mit minimaler maximaler Lateness
\[
\underset{\text{Ablaufpläne}}{\mathrm{argmin}}\left\{ \max_{v \in V}t_L(v)\right\}
\]
*** Latest-deadline-first (LDF)
- iterativ Task einreihen der
- keine uneingereihten nachfolgenden Tasks hat
- die größte Deadline hat
- drehe die Ergebnisliste um
Erzeugt einen Ablaufplan mit minimaler maximaler Lateness
*** Earliest-deadline-first (EDF)
Weitere Bedingungen:
#+begin_definition
$t_r : V \to \mathbb{R}$ ordnet jedem Task den Zeitpunkt zu, ab dem er gestartet werden kann (/Release-Zeit/)
#+end_definition
EDD erzeugt damit Ablaufpläne mit unnötig hoher maximaler Lateness.
Deshalb:
- Nehme an, dass Tasks unterbrochen werden können
- Taskwechsel kosten keine Zeit
1. Springe zum nächsten signifikanten Zeitpunkt (Task fertig oder Task erreicht Release-Zeit)
2. Wähle Task $v^*$ mit kürzester Deadline
Unterscheide:
- der aktuelle Task ist $v^*$ \to v^* läuft weiter
- sonst \to unterbreche den aktuellen Task und starte $v^*$
=goto= 1.
* TODO Systemverifikation
Systeme können *vor* der Einteilung in Hardware/Software beschrieben werden.
** SystemC
- /Module/ realisieren eine konkrete Entität
- /Ports/ erlauben die Kommunikation aus einem Modul heraus
- /Signale/ und /Channels/ modellieren die Kommunikationskanäle
- /Methoden/ führen Operationen aus, getriggert durch Sensitivitätsliste
- /Threads/ führen Operationen aus, starten automatisch
*** 1-Bit Multiplizierer
#+begin_src cpp
SC_MODULE(one_bit_multi){
sc_in a,b;
sc_out f;
void compute() {
f = a && b;
}
SC_CTOR(one_bit_multi) {
SC_METHOD(compute);
sensitive << a << b;
}
};
SC_MODULE(stim_gen){
sc_out a,b;
void send_values() {
a = true;
b = true;
wait(5, SC_NS);
a = false;
b = true;
wait(5, SC_NS);
a = false;
b = false;
wait(5, SC_NS);
}
SC_CTOR(stim_gen) {
SC_THREAD(send_values);
}
};
int sc_main(int, char* []) {
sc_signal a, b, f;
one_bit_multi mul("Multiplizierer");
stim_gen generator("Tester");
mul.a(a);
mul.b(b);
mul.f(f);
generator.a(a);
generator.b(b);
sc_start();
return 0;
}
#+end_src
** TODO Transaction Level Model
Transaktionen sind die Abstraktion der Kommunikation zwischen nebenläufigen Prozessen.
In *SystemC* sind Transaktionen
- /blockierend/
- /nicht-blockierend/
und
- /loosely timed/
- /approximately timed/
- /cycle accurate/