Digitale Hardware/ Software-Systeme- P17

Chia sẻ: Cong Thanh | Ngày: | Loại File: PDF | Số trang:30

Thêm vào BST

Báo xấu

62
lượt xem 4
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Digitale Hardware/ Software-Systeme- P17:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteter Systeme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software- System heutzutage der Stand der Technik. Die Minimierung von Fehlern im Entwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungen unserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation, also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gesteckt als in den eigentlichen Entwurf....

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Digitale Hardware/ Software-Systeme- P17

474 8 Systemveriﬁkation Die Ubergangsmarkierungsfunktion LR : R → 2VR gibt an, f¨ r welchen Zustands¨ ber- ¨ u u gang welches Ereignis v ∈ VR gilt. Dies ist gleichbedeutend mit: Das Ereignis ” LR (s, s ) gilt beim Zustands¨ bergang (s, s )“, wobei ˆ u LR (s, s ) := ˆ v∧ ¬v v∈LR (s,s ) v∈(VR \LR (s,s )) Daneben kann jede SE-LTL-Formel ϕ uber VS und VR auch als LTL-Formel ϕLT L ¨ uber VS ∪ VR interpretiert werden. Dabei sind ϕ und ϕLT L syntaktisch identisch, un- ¨ terscheiden sich aber semantisch. Da jede LTS mit Deﬁnition 8.1.18 als B¨ chi-Automat interpretiert werden kann, u kann, wie im Fall der LTL-Modellpr¨ fung, der Produktautomat aus einer LTS und ei- u nem B¨ chi-Automaten gebildet werden. Sei B = (SB , RB , LB , AB ) ein B¨ chi-Automat u u mit Anfangszust¨ nden SB,0 und M = (S, R, LS , LR ) eine attributierte temporale Struk- a tur mit Anfangszust¨ nden S0 . Der B¨ chi-Automat verwendet die atomaren Aussagen a u VB = VS ∪VR . Der Produktautomat Mp := M ⊗B = (S p , R p , L p , A p ) ist deﬁniert durch: • S p = {(s, sB ) ∈ S×SB | LS (s) ⇒ ∃VR : LB (sB )} (dies beschreibt die Formel LB (sB ), ˆ in der alle Variablen v ∈ VR existentiell quantiﬁziert wurden), v • ((s, sB ), (s , sB )) ∈ R p , genau dann, wenn ∃v ∈ VR : s −→ s ∧ (sB , sB ) ∈ RB ∧ (LS (s) ∧ LR (s, s )) ⇒ LB (sB ) und ˆ ˆ • (s, sB ) ∈ A p , genau dann, wenn sB ∈ AB . Die Anfangszust¨ nde ergebenen sich aus den Paaren der Anfangszust¨ nde beider a a Automaten. Da SE-LTL-Formeln syntaktisch identisch mit LTL-Formeln sind, lassen sich SE-LTL-Formeln als B¨ chi-Automaten modellieren. Somit kann nun die SE-LTL- u Modellpr¨ fung, wie die LTL-Modellpr¨ fung, als Test auf eine leere Sprache des u u Produktautomaten umformuliert werden. Theorem 8.1.1. F¨ r eine LTS M und eine SE-LTL-Formel ϕ gilt: u M |= ϕ ⇔ L(M ⊗ B¬ϕLT L ) = ∅ Die Sprache des Produktautomaten ist deﬁniert, wie in Abschnitt 5.2.2 beschrie- ben. Abstraktion Neben der oben beschriebenen Abbildung von SystemC-Modellen auf parallele Kompositionen von LTS lassen sich weitere Abstraktionen durchf¨ hren, welche die u Veriﬁkationszeit verk¨ rzen k¨ nnen. u o Hardware/Software-Partitionierung Durch Hardware/Software-Partitionierung kann die Modellkomplexit¨ t deutlich re- a duziert werden. Hierzu werden die SystemC-Prozesse in kombinatorische, getaktete und uneingeschr¨ nkte Threads klassiﬁziert und bei der Generierung der LTS geson- a dert behandelt. Kombinatorische Threads besitzen die Eigenschaft, dass diese
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 475 • Sensitiv auf alle Eing¨ nge sind, a • nicht mit dem Taktsignal verbunden sind, • keine wait-Anweisung enthalten und • keine Schleifen ohne konstante Grenzen enthalten. ¨ Kombinatorische Threads werden in eine Formel f ubersetzt und aus dem Modell entfernt. Jedes Mal, wenn Ausgangsvariablen des kombinatorischen Threads gelesen werden, werden diese mit der Formel f beschr¨ nkt. a Getaktete Threads besitzen die Eigenschaft, dass diese • Sensitiv auf eine positive oder negative Taktﬂanke sind, • keine wait-Anweisung mit Argumenten enthalten und • jede Schleife ohne konstante Grenze mindestens eine wait-Anweisung enth¨ lt. a o ¨ Getaktete Threads k¨ nnen in endliche Automaten ubersetzt werden. Hierf¨ r wird u f¨ r den Start, das Ende und jede wait-Anweisung ein Zustand generiert. Die Zu- u stands¨ berg¨ nge werden entsprechend aus den Pfaden im Kontroll-Datenﬂussgra- u a phen des Prozesses erzeugt. Jede τ -Transition der LTS, die diesen Prozess repr¨ sen- a tiert, entspricht einem Zustands¨ bergang in dem endlichen Automaten. u W¨ hrend kombinatorische und getaktete Threads als ungetaktete und getaktete a Hardware-Komponenten angesehen werden k¨ nnen, modellieren uneingeschr¨ nk- o a te Threads Software-Prozesse. Uneingeschr¨ nkte Threads unterliegen erwartungs- a gem¨ ß keinen Einschr¨ nkungen und lassen somit bei der Abbildung auf LTS auch a a keine Optimierungen zu. SAT-basierte Pr¨ dikatenabstraktion a SystemC unterst¨ tzt unterschiedliche Datentypen. Um einen Zugang zum Hardware- u Entwurf zu erleichtern, werden auch Bitvektoren unterst¨ tzt. Die Operationen, die u auf Bitvektoren arbeiten, vergr¨ ßern allerdings den Zustandsraum. Eine m¨ gliche o o Abstraktion kann in diesem Fall durch den Einsatz von arithmetischen Operationen erreicht werden. Erfolgt die Pr¨ dikatenabstraktion durch SAT-Solver (siehe Abschnitt 7.3.3), so a kann die Abstraktion nach folgender Formeln realisiert werden: A A s −→ s ⇔ ∃s, s ∈ S : s −→ s ∧ α (s) = s ∧ α (s ) = s ˆ ˆ ˆ ˆ Dabei ist α die Funktion zur Zustandsabstraktion und S der globale Zustand der par- allelen Komposition der LTS. Die Formel sagt aus, dass ein abstrakter Zustands¨ ber- u gang (s, s ) unter den Ereignissen a ∈ A existiert, sofern im konkreten Modell ein ˆ ˆ Zustands¨ bergang (s, s ) unter den selben Ereignissen existiert und der Start- und u Endzustand Abstraktionen der konkreten Start- und Endzust¨ nde sind. a Thread-modulare Abstraktion Die Repr¨ sentation von SystemC-Modellen durch LTS erfolgt, indem f¨ r jeden a u SystemC-Prozess eine LTS generiert wird und diese anschließend parallel kompo- niert werden. Es kann nun eine Abstraktion des gesamten Modells dadurch erreicht
476 8 Systemveriﬁkation werden, dass zun¨ chst die einzelnen LTS abstrahiert und anschließend parallel kom- a poniert werden. Formal bedeutet dies: Theorem 8.1.2. Sei M die parallele Komposition von n LTS, d. h. M = M1 · · · ˆ ˆ Mn . Sei weiterhin Mi die Abstraktion von Mi und M die Abstraktion von M . Dann gilt: M ≡ M1 · · · Mn ˆ ˆ ˆ Mit anderen Worten: Die Abstraktion der parallelen Komposition der konkreten LTS ¨ ˆ M1 bis Mn ist aquivalent zur parallelen Komposition der abstrakten LTS M1 bis Mn . ˆ Dies bedeutet aber auch, dass die Projektion s|Mi eines Pfades s = s0 , e0 , s1 , e1 , ˜ ˜ . . . in der parallelen Komposition M der LTS M1 bis Mn auf eine einzelne LTS Mi eine Abstraktion von M ist, d. h. (s|Mi ) ˜ M ˜ ˆ Dabei gilt die Projektion s|Mi einer Teilsequenz s von s, die man durch Entfernen der ˜ ˜ Paare (a j , s j+1 ) erh¨ lt, f¨ r alle a j ∈ Vr,i . a u Die beschriebenen Abstraktionen k¨ nnen zu falschnegativen Ergebnissen f¨ hren, o u weshalb f¨ r die Veriﬁkation von SystemC-Modellen eine Abstraktionsverfeinerung u eingesetzt wird [271]. Die Abstraktionsverfeinerung wird dabei durch die Gegenbei- spiele gesteuert, d. h., ergibt die Modellpr¨ fung einer funktionalen Eigenschaft ein u Negativergebnis, wird ein Gegenbeispiel generiert. L¨ sst sich dieses Gegenbeispiel a im urspr¨ nglichen SystemC-Modell jedoch nicht simulieren, so muss das Modell u geeignet verfeinert werden. ¨ 8.1.3 Formale Modellprufung von Transaktionsebenenmodellen Transaktionsebenenmodelle (engl. Transaction Level Model, TLM) werden zuneh- mend als Strukturmodell auf Systemebene eingesetzt. Dabei handelt es sich um eine Netzliste von Prozessoren, Hardware-Beschleunigern, Bussen und Speichern. Die Umsetzung erfolgt dabei h¨ uﬁg in SystemC [352]. a Transaktionen In TLMs werden Transaktionen als Abstraktion der Kommunikation zwischen ne- benl¨ uﬁgen Prozessen verwendet. Transaktionen k¨ nnen entweder atomar oder un- a o terbrechbar sein. Atomare Transaktionen werden in SystemC-TLM als blockierend, unterbrechbare als nichtblockierend bezeichnet. Basierend auf blockierenden und nichtblockierenden Transaktionen deﬁniert SystemC-TLM unterschiedliche Codie- rungsrichtlinien, die als schwach zeitbehaftet (engl. Loosely Timed, LT), approxi- miert zeitbehaftet (engl. Approximately Timed, AT) und zyklenakkurat (engl. Cycle Accurate, CA) bezeichnet werden. In einem LT-TLM werden ausschließlich blockierende Transaktionen (die Sys- temC-Methode b transport) verwendet, die durch einen Start- und einen Endzeit- punkt charakterisiert sind. Diese beiden Zeitpunkte k¨ nnen aber durchaus identisch o
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 477 sein, d. h. die Transaktion hat keine Zeit ben¨ tigt. Ein AT-TLM kann mehrere Trans- o aktionsphasen enthalten und erlaubt somit eine detailliertere Modellierung, etwa von Ressourcenbeschr¨ nkungen. Dies wird durch nichtblockierende Transaktionen a (die SystemC-Methode nb transport) erreicht, f¨ r die SystemC-TLM vier cha- u rakteristische Zeitpunkte deﬁniert: begin request, end request, begin response und end response. Die Deﬁnition eigener Zeitpunkte f¨ r Protokolle mit anderen Phasen u ist aber auch m¨ glich. CA-TLMs sind vergleichbar mit Hardware-Beschreibungen o auf der Registertransferebene und verfeinern AT-TLM mittels eines Taktsignals. AT- und CA-TLMs stellen also Verfeinerungen von LT-TLMs dar und werden aufgrund der h¨ heren Genauigkeit vor allem bei der Veriﬁkation des Zeitverhaltens eingesetzt. o F¨ r die Veriﬁkation funktionaler Eigenschaften werden im Folgenden lediglich LT- u TLMs betrachtet, die mit blockierenden Transaktionen auskommen, was die Notati- on vereinfacht. Außerdem soll die Kommunikation zeitfrei erfolgen. Schwach zeitbehaftete Transaktionsebenenmodelle bestehen aus nebenl¨ uﬁgen a ¨ Prozessen, die uber blockierende Transaktionen miteinander kommunizieren. Die Prozesse k¨ nnen dabei an den Transaktionen blockieren, z. B. aufgrund nicht vor- o handener Daten. Zentral f¨ r die Veriﬁkation von TLMs ist die korrekte Zusammen- u arbeit (Kommunikation) dieser Prozesse. Um funktionale Eigenschaften eines TLM als Anforderungen zu formulieren, m¨ ssen also die zeitlichen Zusammenh¨ nge der u a Transaktionen speziﬁziert werden. Da es in LT-TLMs im Allgemeinen kein Takt- signal gibt, m¨ ssen diese zeitlichen Zusammenh¨ nge relativ zueinander speziﬁziert u a werden. Beispiel 8.1.8. Abbildung 8.11 zeigt m¨ gliche relative zeitliche Zusammenh¨ nge o a zwischen drei blockierenden Transaktionen t1 , t2 und t3 . start bezeichnet dabei den Startzeitpunkt einer Transaktion, end den Endzeitpunkt. Man sieht, dass Transakti- on t3 nach Transaktion t2 und Transaktion t1 startet, da t3 .start > t2 .start > t1 .start. Obwohl Transaktion t2 nach Transaktion t1 startet, wird diese fr¨ her beendet. F¨ r u u die Formulierung von funktionalen Eigenschaften ist es manchmal notwendig, den Abstand zweier Ereignisse zu bestimmen. Ohne Taktsignal kann dies nur relativ zu- einander erfolgen. Beispielsweise ist der Abstand zwischen den Ereignissen t1 .start und t1 .end vier, da drei Ereignisse zwischen diesen liegen. t3 t2 t1 Zeit t1 .start t2 .start t3 .start t2 .end t1 .end t3 .end Abb. 8.11. Drei blockierende Transaktionen in einem LT-TLM [143]
478 8 Systemveriﬁkation M¨ glichen Relationen zwischen zwei Transaktionen in einem LT-TLM sind in o Abb. 8.12 zu sehen. Diese k¨ nnen lediglich anhand der Position eines Start- oder o Endeereignisses einer Transaktion bez¨ glich anderer Ereignisse deﬁniert werden. u Abbildung 8.12a) zeigt, dass Transaktion t1 und Transaktion t2 gleichzeitig statt- ﬁnden, da t1 .start = t2 .start und t1 .end = t2 .end. In Abb. 8.12b) ist der Fall zu se- hen, dass die Transaktion t2 nach t1 startet, beide aber gleichzeitig beendet werden. Abbildung 8.12c) zeigt den Fall, dass die Transaktionen t1 und t2 gleichzeitig star- ten, t1 aber fr¨ her beendet wird, d. h. t1 .start = t2 .start ∧ t1 .end < t2 .end. Schließ- u lich zeigt Abb. 8.12d), dass Transaktion t1 und t2 direkt aufeinander folgen, d. h. t1 .end = t2 .start. a) b) c) d) t2 t2 t2 t2 t1 t1 t1 t1 Zeit t1 .start t1 .end t1 .start t1 .end t1 .start t1 .end t1 .start t1 .end t2 .start t2 .end t2 .start t2 .end t2 .start t2 .end t2 .start t2 .end Abb. 8.12. Beziehungen zwischen Transaktionen in LT-TLMs [143] Formalisierung von LT-TLMs ¨ Die Formalisierung eines SystemC-TLMs erfolgt ahnlich dem in Abschnitt 8.1.2 be- schriebenen Ansatz f¨ r SystemC-Modelle. Da die Synchronisation jetzt nicht mehr u ¨ ¨ ausschließlich uber Ereignisse, sondern uber blockierende Transaktionen erfolgt, wird die Kommunikation ebenfalls formal modelliert. Um den Zustandsraum eines TLM efﬁzient zu modellieren, wird in [345, 347] ein Modell kommunizierender end- licher Automaten vorgestellt. Deﬁnition 8.1.19 (Transaktionsebenenmodell). Ein Transaktionsebenenmodell ist ein Tripel (T MI , T MT , T ), wobei • T MI die Menge an sog. Initiatormodulen, • T MT die Menge an sog. Targetmodulen, und • T ⊆ MI × MT die Menge an Transaktionen SystemC-Module werden in einem TLM als Initiator- oder Targetmodul klassi- ﬁziert. Dabei kann ein Modul tm auch beides sein, d. h. tm ∈ T MI ∧ tm ∈ T MT . Ein Initiatormodul enth¨ lt einen SystemC-Prozess, wobei die Diskussion auf SystemC- a Threads reduziert werden kann. Targetmodule implementieren die Transaktionen
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 479 b transport, weshalb Transaktionen mit Targetmodulen assoziiert werden. An- dererseits k¨ nnen Transaktionen lediglich von Initiatormodulen aufgerufen wer- o den. Welches Initiatormodul welche Transaktion auf welchem Targetmodul aufrufen kann, ist als Paar in der Transaktion gespeichert. Targetmodule, die keine Initiator- module sind, enthalten keinen SystemC-Thread. Beispiel 8.1.9. Ein Beispiel f¨ r ein SystemC-TLM ist in Abb. 8.13 dargestellt. Es u besteht aus sechs Modulen (zwei CPUs, zwei Speicher, ein Bus und ein Arbiter). Die Menge der Initiatormodule T MI besteht aus den beiden CPUs und dem Bus. Die Menge der Targetmodule T MT besteht aus den beiden Speichern, dem Bus und dem Arbiter. Da die beiden Speichermodule und der Arbiter keine Initiatormodule sind, besitzen sie auch keinen SystemC-Thread. Module mit SystemC-Thread sind eingef¨ rbt. a CPU 1 CPU 2 Initiator Initiator Target Bus Target Initiator Initiator Initiator Target Target Target Speicher 1 Speicher 2 Arbiter Abb. 8.13. SystemC-TLM [346] Zur Konstruktion des formalen Modells wird jedes Modul tmi einzeln betrach- ¨ tet und in einem kommunizierenden endlichen Automaten ubersetzt. Analog zu dem Ansatz in Abschnitt 8.1.2 muss der Zustandsraum modelliert werden, in- dem die Variablenbelegungen, die Programmz¨ hler der Prozesse und die Prozess- a zust¨ nde erfasst werden. Die Programmz¨ hler der Prozesse sowie die Variablen- a a belegungen lassen sich als endliche Automaten MPC,i und MPV,i modellieren (sie- he Abschnitt 2.2.2). Enth¨ lt ein Modul keinen SystemC-Thread, wird kein endli- a cher Automat f¨ r den Programmz¨ hler ben¨ tigt. Weiterhin wird f¨ r jede Transaktion u a o u t ∈ {t = (tm,tm ) ∈ T | tm = tmi } ein Initiator-Automat MI,t und f¨ r jede Transakti- u on t ∈ {t = (tm,tm ) ∈ T | tm = tmi } ein Target-Automat MT,t gebildet. Dies ist in Abb. 8.14 zu sehen. Weiterhin zeigt Abb. 8.14 das Zusammenspiel der kommunizierenden endlichen Automaten. Der Automat MPC,1 , der einen SystemC-Thread modelliert, kann somit ¨ Anderungen an der Variablenbelegung vornehmen, indem er mit dem Automaten
480 8 Systemveriﬁkation tm1 t1 tm2 MI,t1 MT,t1 MPV,1 MPC,1 t2 MT,t2 MI,t2 Abb. 8.14. Formales Modell eines SystemC-TLM [346] MPV,1 kommuniziert. Auch kann der SystemC-Thread Transaktionen vom Typ t1 in- itiieren, indem er ein Signal an den Automaten MI,t1 schickt. Das Ergebnis der Trans- ¨ aktion teilt MI,t1 ebenfalls uber ein Signal dem Automaten MPC,1 mit. Die Target- ¨ Automat MT,t2 reagiert auf Transaktionen vom Typ t2 . Diese k¨ nnen Anderungen an o der Variablenbelegung zur Folge haben. Deﬁnition 8.1.20 (Kommunizierende endliche Automaten). Gegeben seien zwei endliche Automaten M1 = (I1 , O1 , S1 , s0,1 , f1 , g1 ) und M2 = (I2 , O2 , S2 , s0,2 , f2 , g2 ) nach Deﬁnition 2.2.13 auf Seite 47 mit Anfangszustand s0,1 bzw. s0,2 . Die beiden Automaten k¨ nnen miteinander kommunizieren, wenn O1 ⊆ I2 und O2 ⊆ I1 ist. o Sei beispielsweise M1 im Zustand s1,1 und M2 im Zustand s1,2 . F¨ hre M1 den u /e Zustands¨ bergang s1,1 −→ s2,1 durch, so w¨ rde M1 in dem Automaten M2 einen u u Zustands¨ bergang aktivieren, wenn ein Zustands¨ bergang mit Eingangssymbol e im u u e Zustand s1,2 existiert, d. h. s1,2 −→ s2,2 . Im Folgenden werden die einzelnen endli- chen Automaten zur formalen Modellierung von TLMs genauer beschrieben. Prozess- und Variablen-Automat Prozess-Automaten modellieren das Verhalten der SystemC-Prozesse, dies ist ver- gleichbar mit dem Programmz¨ hler in dem in Abschnitt 8.1.2 beschriebenen Ansatz. a Hier wird kurz auf die Besonderheiten bei der Modellierung der Kommunikation eingegangen. Beispiel 8.1.10. Gegeben ist ein Initiatormodul mit Port init socket vom Typ tlm initiator socket. Der Prozess ist wie folgt deﬁniert: 1 void process() { 2 while(1) { 3 init_socket.b_transport(data); 4 d++; 5 } 6 }
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 481 o ¨ Die durch b transport ausgel¨ ste Transaktion ubertr¨ gt dabei ein Datum data a vom Typ tlm generic payload. Das Datenfeld von data enth¨ lt den Wert der a Variablen d vom Typ sc uint, einen Bitvektor der Breite zwei. Somit wird ¨ der Wert, der in d gespeichert ist, durch die Transaktion ubertragen. Der resul- tierende Prozess-Automat MPC ist in Abb. 8.15a) zu sehen. Im Anfangszustand s0 wartet der Prozess-Automat auf das Startsignal run, welches vom SystemC- Simulator erzeugt wird. Der Simulator wird sp¨ ter ebenfalls formal modelliert. Hat a der Prozess-Automat das run-Signal empfangen, beginnt die Transaktion durch Er- zeugung des Signals transport start. Erst wenn die Kommunikation beendet wurde (transport end), wird die eigentliche Berechnung des Moduls ausgef¨ hrt, also das u Inkrement der Variable d berechnet. Da hierdurch die Variablenbelegung ge¨ ndert a ¨ wird, erfolgt die Anderung in dem Variablen-Automaten MPV , welcher durch das Signal calculate aktiviert wird. Abbildung 8.15b) zeigt den Variablen-Automaten. a) s0 b) 0 calculate calculate run s1 3 1 transport end / transport start / calculate calculate calculate s2 2 Abb. 8.15. a) Prozess-Automat und b) Variablen-Automat [347] Initiator- und Target-Automat Die Modellierung einer Transaktion erfolgt als Paar von Initiator- und Target-Auto- mat. Der Initiator-Automat reagiert auf das Signal transport start des Prozess- Automaten und initiiert die Kommunikation mittels des Signals request. Der Initiator- Automat wiederholt die Anfrage mit dem selben Signal solange, bis der Target- Automat mit dem Signal response das Ende der Transaktion signalisiert. Der Initiator- Automat ist in Abb. 8.16a) dargestellt. Der korrespondierende Target-Automat ist in Abb. 8.16b) dargestellt. Der Target- Automat verbleibt im Anfangszustand s0 solange, bis das Signal request eine Trans- aktion initiiert. Ob die Transaktion direkt durchgef¨ hrt werden kann, h¨ ngt vom u a ¨ Zustand des Targetmoduls ab, dies wird uber die Variable f signalisiert. Kann die Transaktion momentan nicht durchgef¨ hrt werden (¬ f ), so wird dies dem SystemC- u Simulator mittels des wait-Signals mitgeteilt. Als Argument wird dem SystemC- ¨ Simulator ein Ereignis e ubergeben, welches die Blockierung aufheben kann. Dies veranlasst den SystemC-Simulator, den SystemC-Prozess des Initiatormodul, der die Transaktion initiiert hat, zu blockieren. Die Transaktion kann erst fortgef¨ hrt wer- u den, wenn der SystemC-Simulator das Signal run erzeugt. Ist die Bedingung zur
482 8 Systemveriﬁkation a) s0 b) s0 request ∧¬ f response transport start response request / wait(e) / request / request ∧f s1 s2 s1 run ¬ response / request Abb. 8.16. a) Initiator-Automat und b) Target-Automat [347] Abarbeitung der Transaktion direkt gegeben ( f ), wird die Transaktion durchgef¨ hrt. u Die Beendigung der Transaktion wird durch das Signal response angezeigt. Man beachte, dass durch den Zustand s1 das Blockieren eines SystemC-Prozesses modelliert wird. Dieser Mechanismus kann auch f¨ r wait-Anweisungen im Sys- u temC-Prozess angewendet werden. Modellierung des SystemC-Simulators Schließlich muss noch der SystemC-Simulator selbst modelliert werden. Der im Fol- genden vorgestellte Ansatz unterscheidet sich von dem in Abschnitt 8.1.2 dadurch, dass dynamische Sensitivit¨ tslisten unterst¨ tzt werden und Zeitbetrachtungen mit a u aufgenommen werden k¨ nnen. o Der SystemC-Simulator wird ebenfalls als endlicher Automat modelliert und realisiert die Ablaufplanung nach dem SystemC-Standard [236]. Ein SystemC- Simulator f¨ r n SystemC-Prozesse p1 , . . . , pn ist ein endlicher Automat, wobei die u Zust¨ nde mit Trippeln (σ , π , φ ) markiert sind. Dabei ist a • σ ∈ {⊥, p1 , . . . , pn } die Prozessauswahl , die eventuell leer ist (⊥), • π := (π1 , . . . , πn ) der Zustandsvektor aller n Prozesse, mit dem Prozesszustand πi ∈ {bereit, lau f end, blockiert} f¨ r jeden SystemC-Prozess pi , und u • φ ∈ {evaluate, update, delta noti f y,timed noti f y} zeigt die Ablaufplanungs- phase an. Die Initialisierung des Simulators erfolgt als s0 = (⊥, bereit, . . . , bereit, evaluate) Somit startet der Simulator in der Evaluierungsphase, in der alle Prozesse bereit sind. Der SystemC-Simulator wird im n¨ chsten Schritt einen Prozess pi ausw¨ hlen a a und ausf¨ hren, d. h. die Prozessauswahl wird auf σ = pi aktualisiert und pi geht in u den Prozesszustand πi = lau f end uber. Prozess pi wird ausgef¨ hrt, bis er die n¨ chste ¨ u a wait-Anweisung erreicht. Dabei geht er in den Prozess-Zustand πi = blockiert uber ¨ und die Prozessauswahl wird auf σ =⊥ gesetzt. Der Simulator w¨ hlt so lange Prozesse aus und f¨ hrt diese aus, bis kein Prozess a u mehr im Prozesszustand bereit ist, d. h.
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 483 σ =⊥ ∧∀1 ≤ i ≤ n : πi = blockiert Daraufhin schaltet der SystemC-Simulator in die Ablaufplanungsphase φ = update. In dieser Phase werden die SystemC-Kan¨ le aktualisiert, dies bedeutet, dass die Va- a riablen f in Abb. 8.16b) neu bewertet werden. Anschließend wechselt der SystemC- Simulator in die Ablaufplanungsphase φ = delta noti f y. Dies hat zur Folge, dass alle Ereignisse, die w¨ hrend der Evaluierungsphase f¨ r den n¨ chsten Delta-Zyklus a u a erzeugt wurden, nun sichtbar werden. Damit werden alle Prozesse pi mit πi = blockiert, die auf ein solches Ereignis warten, auf πi = bereit gesetzt werden. Schließlich erfolgt der Wechsel des SystemC-Simulators in die Ablaufplanungspha- se φ = evaluate. Wird allerdings kein Prozess laufbereit, so wechselt der SystemC- Simulator zun¨ chst in den Zustand timed notify und die Simulationszeit wird auf den a n¨ chste Zeitpunkt gesetzt, zu dem ein Ereignis auftritt. a Beispiel 8.1.11. Abbildung 8.17 zeigt die Prozesszustands¨ berg¨ nge f¨ r den Prozess u a u aus Beispiel 8.1.10. Der Prozesszustand πi wird von bereit auf laufend gesetzt, so- bald der Prozess pi ausgew¨ hlt wurde (σ = pi ) und Signal run erzeugt wird. Beim a Erreichen einer wait-Anweisung blockiert der Prozess an dem zugeh¨ rigen Ereignis o e. Erst das Auftreten von e kann den Prozess wieder in den Zustand bereit versetzen. laufend σ = pi wait(e) / run bereit blockiert e Abb. 8.17. Prozesszustands¨ berg¨ nge f¨ r den Prozess pi aus Beispiel 8.1.10 [347] u a u Modellierung von Kan¨ len a Die Ber¨ cksichtigung von Kan¨ len verlangt, dass der in SystemC verwendete re- u a quest/update-Mechanismus umgesetzt wird. Dies erfolgt wiederum in einem endli- chen Automaten (siehe Abb. 8.18a)) und zwar f¨ r jeden Kanal einzeln. Der Automat u startet im Zustand s0 . Wird eine Kanalaktualisierung angezeigt, d. h. ein Prozess hat eine Transaktion auf dem Kanal durchgef¨ hrt, geht der jeweilige Automat in u ¨ den Zustand s1 uber. Wechselt der SystemC-Simulator in die Ablaufplanungsphase φ = update, so wechseln alle Automaten von ge¨ nderten Kan¨ len in den Zustand a a s2 , in welchem die eigentliche Aktualisierung stattﬁndet. Diese Aktualisierung ist kanalspeziﬁsch und deshalb nicht in Abb. 8.18a) dargestellt. Die Beendigung der ¨ Aktualisierung erfolgt durch Uberg¨ nge nach s0 und senden von done-Signalen. a
484 8 Systemveriﬁkation a) s0 b) s0 request / done cancel notify s2 s1 s1 σ = update Abb. 8.18. a) Modellierung der Kanalaktualisierung und b) Modellierung von Ereignissen [347] Modellierung von Ereignissen Jedes SystemC-Ereignis wird ebenfalls als endlicher Automat modelliert. Dieser ist in Abb. 8.18b) dargestellt. Bei der Erzeugung eines Ereignisses durch eine notify- Anweisung wird das Ereignis notify erzeugt, was den Zustands¨ bergang nach s1 ver- u ursacht. Dieser Zustand zeigt an, dass ein Ereignis sp¨ ter sichtbar werden soll. Durch a Aufruf einer cancel-Anweisung kann dieser Zustand wieder verlassen werden, bevor der Simulator das Ereignis ber¨ cksichtigt. u Dieses formale Modell kommunizierender Automaten erfasst das Verhalten be- u u ¨ liebiger SystemC-TLMs. F¨ r die Modellpr¨ fung kann die Ubersetzung eines Mo- dells eines SystemC-TLMs in eine temporale Struktur erfolgen [347]. Alternativ ist ¨ eine Ubersetzung auf attributierte temporale Strukturen denkbar. ¨ ¨ 8.1.4 Zusicherungsbasierte Eigenschaftsprufung fur Transaktionsebenenmodelle Auf der Register-Transfer-Ebene werden Zusicherungen als Sequenzen Boolescher ¨ Ausdr¨ cke uber beobachtete Signalwerte beschrieben. Die Auswertung einer Se- u quenz erfolgt dann mittels eines Monitors synchron zum SUV (engl. System Under Veriﬁcation). Dabei wird der Wechsel eines Taktsignals oder eines anderweitig ge- eigneten Signals verwendet, um diejenigen Zeitpunkte zu bestimmen, an denen die Booleschen Ausdr¨ cke auszuwerten sind. Auf Transaktionsebene werden Modelle u abstrakter modelliert und Ereignisse weitestgehend vermieden, um Kontextwech- sel zum Simulator zu vermeiden. Nur an denjenigen Stellen, wo es zu Konﬂikten im Daten- oder Kontrollﬂuss kommen kann, werden Ereignisse zur Synchronisation eingesetzt. Dies hat aber auch zu Folge, dass in der Regel kein Taktsignal verf¨ gbar u ist, um die Zeitpunkte zur Evaluierung zu bestimmen. Aus diesem Grund ist es not- wendig, geeignete Ereignisse im TLM zu generieren. In [361] ist ein Ansatz beschrieben der auf dem sog. engl. Observer Pattern ba- siert. Jeder Monitor verwendet einen Observer, um diejenigen Kan¨ le und Signale im a ¨ SUV zu beobachten, die er zur Uberpr¨ fung der Zusicherung ben¨ tigt. Dabei kann u o ein Observer-Objekt von mehreren Monitoren verwendet werden. Weiterhin kann ein Kanal oder ein Signal von mehreren Observern beobachtet werden. Damit die Ob- ¨ ¨ server uber relevante Ereignisse (hierzu geh¨ ren auch Anderungen am Status eines o
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 485 Kanals) informiert werden, ist es notwendig, die verwendeten Kommunikationsme- ¨ thoden (nb transport, b transport etc.) zu uberladen. Dies wird an dem Beispiel aus [361] f¨ r einen einfachen FIFO-Kanal illustriert. u Beispiel 8.1.12. Es wird lediglich die Leseoperation read betrachtet. Der FIFO- Kanal ist vom Typ fifo. Ohne die genaue Implementierung des FIFO-Kanals zu kennen, kann die Leseoperation beobachtbar gemacht werden, indem von fifo ein neuer Typ observable fifo abgeleitet wird. 1 class observable_fifo : public fifo, observer { 2 public: 3 observable_fifo(sc_module_name name) : fifo(name) {}; 4 void read(char& c) { 5 fifo::read(c); 6 obs_notify(&c); 7 } 8 }; In Zeile 3 ist der Konstruktor des beobachtbaren FIFO-Kanals implementiert, indem lediglich der Default-Konstruktor der urspr¨ nglichen FIFO-Klasse aufgerufen wird. u ¨ In Zeile 4 wird die Methode read uberladen. Diese ruft die originale read-Methode auf und benachrichtigt alle registrierten Observer in Zeile 6. Zur Generierung der Monitore auf Transaktionsebene kann dann das in Ab- schnitt 6.4.1 beschriebene Verfahren angewandt werden, wobei komplexe Monitore aus elementaren Monitoren zusammengesetzt werden. Dabei ist die Verwendung ei- nes Taktsignals nicht mehr n¨ tig. Dies wird ebenfalls anhand eines Beispiels [361] o illustriert. ¨ Beispiel 8.1.13. Es soll ein elementarer Monitor zur Uberpr¨ fung der PSL-Formel u always expr gebaut werden. Eine Implementierung in C++ kann dann wie folgt aus- sehen: 1 class monitor_always : public monitor { 2 protected: 3 bool reset_n, start, expr, checking, valid, 4 start_always, start_t, valid_t; 5 6 public: 7 monitor_always(const char* name) : monitor(name) { 8 valid_t = true; 9 } 10 void update() { 11 start_always = start || start_t; 12 if ((!reset_n) || (!start_always)) 13 valid_t = true; 14 else
486 8 Systemveriﬁkation 15 if (expr) 16 valid_t = true; 17 else 18 valid_t = false; 19 if (!reset_n) 20 start_t = false; 21 else 22 if (start) 23 start_t = true; 24 valid = valid_t; 25 checking = start_always; 26 } 27 }; Die Variablen reset n, start und expr sind die Eingangssignale des Monitors und k¨ nnen von außerhalb des Monitors geschrieben werden. Die Methode update o ¨ wird nach jeder Anderung an einem dieser drei Signale aufgerufen. Die Ausgabe des Monitors sind die Signale checking und valid (wie bereits in Abschnitt 6.4.1 eingef¨ hrt). u Die Variable start t wird verwendet, um ein einmal gegebenes Startsignal bis zum n¨ chsten Zur¨ cksetzen zu speichern. Somit zeigt die in Zeile 11 berechnete Va- a u ¨ ¨ riable start always an, ob uberhaupt eine Uberpr¨ fung bei dem aktuellen Aufruf u von update() durchgef¨ hrt wird. Falls dies nicht der Fall ist oder gerade ein akti- u ves R¨ cksetzsignal (reset) anliegt, wird die Variable valid t auf den Default-Wert u ¨ true gesetzt (Zeile 12 und 13). Andernfalls wird in den Zeilen 15 bis 18 uberpr¨ ft, u ob expr erf¨ llt ist. Die Ausgabe wird erst in den Zeilen 24 und 25 erzeugt. u Man sieht, dass die Monitore als C++-Klassen implementiert werden k¨ nnen. o ¨ Da diese uber den Observer gesteuert werden, ﬁnden keine Kontextwechsel durch Monitore statt, was ansonsten einen enormen Overhead an Simulationszeit w¨ hrend a der Veriﬁkation zur Folge h¨ tte. a Die Konstruktion komplexer Monitore f¨ r PSL-Zusicherungen erfolgt mit dem u in [361] beschriebenen Ansatz durch Verschaltung elementarer Monitore (siehe auch Abschnitt 6.4.1). Dies wird anhand eines Beispiels aus [361] illustriert. Beispiel 8.1.14. Abbildung 8.19a) zeigt ein Transaktionsebenenmodell eines Produ- cer/Consumer-Systems. Der Produzent (engl. producer) erzeugt Nachrichten, wel- che aus einzelnen Zeichen bestehen, und schreibt diese in einen FIFO-Kanal. Eine Nachricht beginnt stets mit dem Symbol %“ und endet mit dem Zeichen $“. Der ” ” Konsument (engl. consumer) liest die Nachrichten als Sequenz von Zeichen aus dem ¨ FIFO-Kanal. Es soll nun gezeigt werden, dass die Ubertragung einer neuen Nach- richt erst beginnt, nachdem die vorherige Nachricht vollst¨ ndig geschrieben wurde. a Mit Hilfe des in Beispiel 8.1.12 eingef¨ hrten Monitors, kann dies als PSL- u Zusicherung formuliert werden. assert always ((char == % ) -> next((not(char == % )) until! (char == $ )))
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 487 a) Producer FIFO Consumer b) Wrapper 1 always -> next until! operand operand checking checking checking checking operand start start start valid Abb. 8.19. PSL-Monitor f¨ r ein TLM eines Producer/Consumer-System [361] u Die Methode read des FIFO-Kanals mit beobachtbarer Leseoperation kann mittels einer C++-Klasse das gelesene Zeichen char zur¨ ckliefern. Da PSL neben VHDL u und SystemVerilog ebenfalls SystemC unterst¨ tzt, kann dieses Zeichen direkt zum u Vergleich gegen das Start- und Endezeichen einer Nachricht innerhalb einer PSL- Zusicherung verwendet werden. Die Umsetzung der PSL-Zusicherung erfolgt durch Verschaltung elementarer Monitore [361]: 1 class monitor_msg_seq : public monitor { 2 public: 3 monitor_msg_seq(const char* name) : monitor(name) { 4 mnt_always = new monitor_always("always"); 5 mnt_imply = new monitor_imply("->"); 6 mnt_next = new monitor_next("next", WEAK, 1); 7 mnt_until = new monitor_until("until!", STRONG); 8 ... 9 }; 10 void update() { 11 expr_0 = (char == ’%’); 12 expr_1 = !(char == ’%’); 13 expr_2 = (char == ’$’); 14 mnt_until->update(); 15 valid = valid_i; 16 checking = checking_i; 17 ... 18 } 19 };
488 8 Systemveriﬁkation Im Konstruktor monitor msg seq werden die elementaren Monitore instantiiert. Hierbei wird auch der Always-Monitor aus Beispiel 8.1.13 verwendet. Der Until- und Next-Monitor erhalten zus¨ tzliche Argumente, die anzeigen, ob es sich um einen a schwachen oder einen starken Operator handelt. Der Next-Operator bekommt zus¨ tz- a lich die Anzahl an Zeitschritten mitgeteilt, nach denen die zugeh¨ rige Teilformel o ausgewertet werden soll. Die Zeitschritte ergeben sich aus dem Ereignis, welches in der read-Methode des FIFO erzeugt wird. In der Methode update werden die aus- zuwertenden Ausdr¨ cke gesetzt. Anschließen wird die Auswertung des am weitesten u rechts stehenden Until-Monitors gestartet (Zeile 14), der wiederum die angeschlosse- nen Monitore startet. Die Ausgabe des Until-Monitors (valid i und checking i) wird mit den Ausg¨ ngen valid und checking des zusammengesetzten Monitors a verbunden. Ein weiteres Beispiel [361] soll die zusicherungsbasierte Eigenschaftspr¨ fung u von Transaktionsebenenmodellen verdeutlichen. Beispiel 8.1.15. Abbildung 8.20 zeigt ein System bestehend aus einer CPU, einem DMA-Controller (engl. direct memory access), zwei Speicher-Modulen und einem ¨ Bus. In dem DMA-Controller gibt es vier Register, die uber bestimmte Adressen an- gesprochen werden k¨ nnen. F¨ r Kopieroperationen zwischen den beiden Speicher- o u modulen wird der DMA-Controller von der CPU wie folgt programmiert: 1. Zun¨ chst schreibt die CPU die Quelladresse in das zugeh¨ rige DMA-Register a o source. 2. In einem zweiten Schritt wird die Zieladresse von der CPU in das DMA-Register sink geschrieben. 3. Anschließend speichert die CPU die L¨ nge des zu kopierenden Blocks in das a DMA-Register length. 4. Schließlich initiiert die CPU den Transfer durch setzten des DMA-Kontrollre- gisters control. Alle Kopieroperationen werden von der CPU initiiert und mittels b transport- Aufrufen realisiert. Das eigentliche Kopieren der Daten f¨ hrt der DMA-Controller u dabei selbst¨ ndig durch alternierende Lese- und Schreiboperationen aus. Die Been- a digung des Kopiervorgangs signalisiert der DMA-Controller der CPU mittels eines Interrupt-Signals dma irq. Dieses Interrupt-Signal ist im TLM als ein Signal imple- mentiert. Das Interrupt-Signal wird von der CPU gel¨ scht, indem das Kontrollregis- o ter im DMA-Kontroller zur¨ ckgesetzt wird. u Im Folgenden werden vier PSL-Zusicherungen f¨ r dieses Modell vorgestellt. Da- u bei wird einfachheitshalber davon ausgegangen, dass Kopieroperationen stets vom Speicher 1 (mem1) in den Speicher 2 (mem2) erfolgen. Die erste Zusicherung besagt, ¨ ¨ dass nach der Ubertragung der Quelladresse als n¨ chste Transaktion die Ubertragung a der Zieladresse erfolgt. Hierzu muss der Initiator-Socket cpu init socket der CPU ¨ ¨ uberwacht werden. Dies erfolgt durch Uberladen der b transport-Implementierung und die Verwendung eines Wrapper-Moduls. Die PSL-Zusicherung kann dann wie folgt formuliert werden:
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 489 CPU DMA-Controller dma irq Initiator Initiator Target Target Bus Target Initiator Initiator Initiator Target Target Speicher 1 Speicher 2 Abb. 8.20. SystemC-TLM f¨ r DMA-Speicherzugriffe u assert always ((cpu init socket.isWritten()&&(writtenAddr == source)) -> (next (next event(cpu init socket.isWritten()) (writtenAddr == sink)))); Die zweite Zusicherung fordert, dass jedes Mal, nachdem das Kontrollregister des DMA-Controller geschrieben wurde (nicht zur¨ ckgesetzt wurde), das Interrupt- u Signal dma irq gesetzt werden muss, bevor das Kontrollregister wieder geschrieben wird. assert always ((cpu init socket.isWritten()&&(writtenAddr == control)&& (writtenData! =reset)) -> (next (dma irq before (cpu init socket.isWritten()&&(writtenAddr == control))))); Schließlich soll gezeigt werden, dass die Lese- und Schreiboperationen zwischen den beiden Speichern alternieren: assert always (next event(mem1.isRead()) (next (mem2.isWritten() before mem1.isRead()))) Die vierte Zusicherung schließlich fordert, dass die verwendete decodierte Lese- adresse (decodedAddr) identisch ist mit der von der CPU geschriebenen Leseadres- se (readAddr). assert always ((cpu init socket.isWritten()&&(writtenAddr == source)) -> (next event!(mem1.isRead()) (readAddr == decodedAddr)));
490 8 Systemveriﬁkation 8.2 Zeitanalyse auf Systemebene Eingebettete Systeme werden zunehmend als heterogene Multiprozessorsysteme entworfen. In einem solchen System sind die Komponenten oftmals hoch optimiert, um die Anforderungen zu erf¨ llen, die sich aus der Umgebung und der zu erbrin- u genden Funktionalit¨ t ergeben. Dies gilt sowohl f¨ r die Prozessoren und Hardware- a u Beschleuniger als auch f¨ r die Kommunikationsbusse und Speicher. Hieraus er- u gibt sich, dass der Entwurf und die Veriﬁkation eingebetteter Systeme zunehmend schwieriger wird. Dabei beschr¨ nkt sich die Veriﬁkation nicht nur auf funktiona- a le Eigenschaften, wie Gefahrlosigkeit und Lebendigkeit, sondern sie muss auch die Korrektheit des Zeitverhaltens garantieren. Um die Komplexit¨ t der Zeitanalyse auf Systemebene zu verstehen, muss man a die Entscheidungen im Systementwurf kennen, da diese Einﬂuss auf das Zeitver- halten der Implementierung haben. Typische Entwurfsentscheidungen auf Systeme- bene sind [426]: Die Partitionierung in Hardware- und Software-Komponenten, die Allokation der Prozessoren, die Bindung von Prozessen an die Komponenten, die Abbildung von Daten in Speicher, das Routing von Speicherzugriffen sowie die Ab- laufplanung von Prozessen und Transaktionen auf gemeinsam genutzten Ressourcen. Alle diese Entwurfsentscheidungen haben Einﬂuss auf das Zeitverhalten der Imple- mentierung und m¨ ssen daher in einer Zeitanalyse ber¨ cksichtigt werden. Dies ist u u im Y-Diagramm in Abb. 8.21 dargestellt. Verhalten Anforderungen Entwurfsent- scheidungen & Verfeinerung Zeitanalyse Entwurfsraum- exploration Abb. 8.21. Y-Diagramm Ausgehend von dem Verhaltensmodell und den Anforderungen der Speziﬁkati- on werden die oben beschriebenen Entwurfsentscheidungen getroffen und das Ver- haltensmodell verfeinert. Die resultierende Implementierung ist die Eingabe f¨ r u die Zeitanalyse, deren Ergebnisse im Entwurfsprozess zur Steuerung der Optimie-
8.2 Zeitanalyse auf Systemebene 491 rung verwendet werden. Man beachte, dass das Y-Diagramm Teilaspekte der X- Diagramme f¨ r den Entwurf und f¨ r die Veriﬁkation zusammenfasst. Weiterf¨ hrende u u u Erl¨ uterungen zum Entwurfsprozess und zur Entwurfsraumexploration ﬁnden sich in a [426] und werden hier nicht n¨ her erl¨ utert. a a Das Veriﬁkationsziel bei der Pr¨ fung von Zeiteigenschaften kann entweder der u Beweis oder die Falsiﬁkation der Eigenschaften sein. Bei der Falsiﬁkation werden solange neue Ergebnisse mit der Zeitanalyse ermittelt und mit den Anforderungen verglichen, bis ein Gegenbeispiel gefunden ist bzw. bis der Entwickler soviel Ver- trauen in die Implementierung hat, dass keine weiteren Bewertungen vorgenom- men werden. Die Zeitanalyse spielt hierbei unterschiedliche Szenarien durch, um m¨ glichst schnell ein Gegenbeispiel zu generieren. Ist das Veriﬁkationsziel der Be- o weis, so liefert die Zeitanalyse sog. Zeitschranken zur¨ ck (siehe auch Abb. 7.28 auf u Seite 433). Zeitschranken sind minimale und maximale Werte f¨ r Zeiteigenschaften, u wie Latenz, Durchsatz etc. Man spricht in diesem Zusammenhang auch von unteren und oberen Zeitschranken. Die ermittelten Zeitschranken werden mit den Zeitanfor- derungen verglichen, und nur, wenn die Zeitschranken keine Anforderung verletzen, ist der Beweis erbracht, dass das System die Zeitanforderungen erf¨ llt. u Aus dem Y-Diagramm lassen sich Kriterien f¨ r Verfahren zur Zeitanalyse auf u Systemebene ableiten [435]: • Korrektheit: Die Ergebnisse der Zeitanalyse m¨ ssen korrekt sein. Handelt es sich u bei dem Veriﬁkationsziel um einen Beweis, so muss das Ergebnis der Zeitanaly- se f¨ r alle erreichbaren Systemzust¨ nde und alle m¨ glichen Eingaben gelten. So u a o darf beispielsweise die obere Schranke f¨ r eine Latenz die tats¨ chlich maximale u a Antwortzeit eines Systems nicht unterschreiten. Handelt es sich bei dem Veri- ﬁkationsziel um eine Falsiﬁkation, so muss das erbrachte Gegenbeispiel, eine zul¨ ssige Eingabe f¨ r die Implementierung darstellen. a u • Genauigkeit: Um falschnegative und falschpositive Ergebnisse zu verhindern, m¨ ssen die Ergebnisse der Zeitanalyse genau genug sein. Dies bedeutet, dass u die berechneten unteren und ober Schranken m¨ glichst genau den tats¨ chlich o a minimal und maximal erreichbaren Zeiteigenschaften entsprechen bzw. das Ge- genbeispiel genau genug ist, so dass es auch in einem gefertigten System poten- tiell gilt. Beispielsweise kann eine obere Schranke an die Latenz beliebig hoch gesetzt werden, ohne das die tats¨ chliche maximale Antwortzeit des Systems a unterschritten wird (Korrektheit). Allerdings hilft eine solche willk¨ rlich hohe u Schranke nicht, das System angemessen auszulegen. • Anwendbarkeit: Damit eine Zeitanalyse f¨ r eine Vielzahl an Systemen anwend- u bar ist, muss sie m¨ glichst alle oben genannten Entwurfsentscheidungen re- o pr¨ sentieren k¨ nnen. Dar¨ ber hinaus muss eine Zeitanalyse eine m¨ glichst große a o u o Klasse an Berechnungsmodellen f¨ r die Modellierung des Verhaltens unterst¨ t- u u zen. • Geschwindigkeit: Schließlich sollten die Ergebnisse der Zeitanalyse m¨ glichst o schnell vorliegen, um w¨ hrend der Entwurfsraumexploration eine Vielzahl an a L¨ sungen bewerten zu k¨ nnen. o o
492 8 Systemveriﬁkation Wie im Fall der bisher vorgestellten Methoden zur funktionalen Veriﬁkation, ist es im Allgemeinen auch im Fall der Zeitanalyse nicht m¨ glich, alle oben genannten o Kriterien zu erf¨ llen. Bei der Zeitanalyse k¨ nnen die verwendeten Verfahren wieder- u o um in simulative und formale Methoden eingeteilt werden. Wie bei der funktionalen Veriﬁkation gilt auch hier, dass simulative Methoden unvollst¨ ndig sind und sich so- a mit im Allgemeinen nur f¨ r das Veriﬁkationsziel der Falsiﬁkation eignen. Formale u Methoden zur Zeitanalyse k¨ nnen wiederum f¨ r das Veriﬁkationsziel eines Bewei- o u ses verwendet werden. Auch sonst stehen die oben genannten Kriterien im Konﬂikt zueinander, weshalb eine Zeitanalysemethode nicht alle Kriterien in vollem Umfang erf¨ llen kann. Unabh¨ ngig davon, ob simulative oder formale Methoden eingesetzt u a werden, wird im Allgemeinen eine h¨ here Genauigkeit mit einer l¨ ngeren Laufzeit o a einhergehen. Andererseits bedeutet eine h¨ here Anwendbarkeit auch in der Regel o eine Einschr¨ nkung in der Korrektheit der Methode. a Im Folgenden werden nun simulative und formale Methoden zur Zeitanalyse auf Systemebene vorgestellt. Zun¨ chst wird ein simulatives Verfahren vorgestellt, a welches eine Vielzahl an Entwurfsentscheidungen ber¨ cksichtigen kann und somit u f¨ r die Zeitbewertung moderner eingebetteter Systeme auf Systemebene geeignet u ist. Der Nachteil ist allerdings, dass dieses Verfahren, wie alle anderen simulativen Ans¨ tze, unvollst¨ ndig ist. Anschließend werden zwei formale Methoden zur Zeit- a a analyse auf Systemebene vorgestellt. Das erste der beiden Verfahren ist eine kompo- sitionale Zeitanalyse, die Ereignisstr¨ me zur Kopplung bestehender Planbarkeitsana- o lysen f¨ r Einprozessorsystemen verwendet. Das zweite Verfahren ist eine modulare u Zeitanalyse basierend auf Ankunfts- und Servicekennlinien. 8.2.1 Simulative Zeitbewertung Ein Ansatz zur simulativen Zeitanalyse der direkt dem Y-Diagramm in Abb. 8.21 entspricht, ist an der Universit¨ t Erlangen-N¨ rnberg entwickelt und in das Entwurfs- a u system SystemCoDesigner zur Entwurfsraumexploration und Systemsynthese inte- griert worden [215, 216, 254]. F¨ r die Speziﬁkation erwartet das Entwurfssystem u ein ausf¨ hrbares SysteMoC-Verhaltensmodell (siehe Abschnitt 2.3.2). Entwurfsbe- u schr¨ nkungen werden in Form einer Plattform, modelliert als Architekturgraph, und a Bindungsbeschr¨ nkungen angegeben. Die Entwurfsraumexploration mit SystemCo- a Designer erfolgt vollautomatisch, wobei mehrere Zielgr¨ ßen gleichzeitig optimiert o werden k¨ nnen. F¨ r die Absch¨ tzung des Zeitverhaltens w¨ hrend der Exploration o u a a werden aus dem SysteMoC-Modell und den Entwurfsentscheidungen automatisch zeitbehaftete SystemC-Modelle generiert. Um dabei die Explorationszeiten gering zu halten, erfolgt die Erstellung des zeitbehafteten Modells per Konﬁguration und bedarf keiner Neukompilation des Modells. Virtual Processing Components (VPC) Der in SystemCoDesigner verwendete Ansatz zur Absch¨tzung des Zeitverhaltens a ist eine simulative Zeitanalyse, basierend auf einer SystemC-Bibliothek mit dem Na- men VPC (engl. Virtual Processing Components). Das Verhaltensmodell ist in Sys- teMoC programmiert. Es handelt sich dabei um ein rein funktionales Modell, ohne
8.2 Zeitanalyse auf Systemebene 493 ¨ jegliche Informationen uber nichtfunktionale Eigenschaften wie Zeitverhalten. Da SysteMoC-Modelle ausf¨ hrbare Verhaltensmodelle sind, k¨ nnen sie entsprechend u o zur Simulation des Verhaltens verwendet werden. Die allozierten Komponenten der Plattform, z. B. Prozessoren, Hardware-Beschleuniger, Speicher, Busse, werden als virtuelle Komponenten (engl. Virtual Processing Components, VPCs) modelliert. Je- de VPC repr¨ sentiert somit eine Komponente der Plattform. Technisch sind VPCs als a SystemC-Module in einer SystemC-Bibliothek, der sog. VPC-Bibliothek realisiert. VPCs sind in der Simulation daf¨ r zust¨ ndig, die Ausf¨ hrung von Aktoren entspre- u a u a u o ¨ chend ihrer gesch¨ tzten Ausf¨ hrungszeiten zu verz¨ gern, d. h. VPCs ubernehmen die Zeitsimulation. Zur Kopplung der Anwendung mit der Plattform, m¨ ssen SysteMoC-Aktoren u entsprechend der Entwurfsentscheidungen an VPCs gebunden werden. Dies erfolgt in zwei Schritten: 1. Jede VPC erh¨ lt die auf tieferen Abstraktionsebenen gesch¨ tzten Ausf¨ hrungs- a a u zeiten derjenigen Aktoren, die an die entsprechende Ressource gebunden sind. 2. Funktionen in SysteMoC-Aktoren werden am Ende der Funktion mit einem Funktionsaufruf erg¨ nzt, der die weitere Ausf¨ hrung des Aktors an derjenigen a u VPC blockiert, an die der Aktor gebunden wurde. Das Ergebnis dieser beiden Schritte ist ein kombiniertes Simulationsmodell, wel- ches sowohl das funktionale Verhalten als auch das Zeitverhalten simuliert. Bei den Ausf¨ hrungszeiten handelt es sich um die gesch¨ tzten Zeiten f¨ r die Ausf¨ hrung der u a u u Kernfunktionalit¨ t (engl. core execution times), also derjenigen Zeit, die zur Berech- a nung des Aktors ohne Unterbrechung durch externe Ereignisse ben¨ tigt wird. o Die Ausf¨ hrungssemantik eines einzelnen SysteMoC-Aktors, mit endlichen Au- u tomaten M, in einer kombinierten Verhaltens- und Zeit-Simulation ist damit wie folgt: 1. Initialisierung: Der aktuelle Zustand des endlichen Automaten M wird auf den Anfangszustand gesetzt. 2. Pr¨ dikatenevaluierung: Alle Bedingungen von aus dem aktuellen Zustand aus- a gehenden Zustands¨ berg¨ ngen des endlichen Automaten M werden evaluiert. u a 3. Funktionsausf¨ hrung: Ein Zustands¨ bergang aus dem aktuellen Zustand, des- u u sen Pr¨ dikat erf¨ llt ist, wird nichtdeterministisch ausgew¨ hlt, und die annotierte a u a a u ¨ Funktion berechnet. Ist kein Pr¨ dikat erf¨ llt, wartet der Aktor auf eine Anderung der F¨ llst¨ nde der angeschlossenen Kan¨ le und f¨ hrt dann seine Ausf¨ hrung in u a a u u Schritt 2. fort. 4. Zeitsimulation: Durch Aufruf der VPC, an die der Aktor gebunden ist, blockiert ¨ der Aktor und die VPC ubernimmt die Zeitsimulation. 5. Zustands¨ nderung: Entsprechend dem Pr¨ dikat des ausgew¨ hlten Zustands¨ ber- a a a u gangs werden Daten konsumiert und produziert sowie der Folgezustand gesetzt. Die Ausf¨ hrung wird mit Schritt 2. fortgesetzt. u Bei der beschriebenen Ausf¨ hrungssemantik sieht man, dass Funktionen atomar also u ohne Unterbrechung berechnet werden. Hierdurch werden Seiteneffekte vermieden, ¨ die evtl. den in Variablen gespeicherten Zustand andern k¨ nnten. o