Wydział Informatyki - Informatyka (N2)
specjalność: grafika komputerowa i systemy multimedialne
Sylabus przedmiotu Testowanie i weryfikacja systemów sprzętowo-programowych - Przedmiot obieralny II:
Informacje podstawowe
| Kierunek studiów | Informatyka | ||
|---|---|---|---|
| Forma studiów | studia niestacjonarne | Poziom | drugiego stopnia |
| Tytuł zawodowy absolwenta | magister | ||
| Obszary studiów | nauki techniczne | ||
| Profil | ogólnoakademicki | ||
| Moduł | — | ||
| Przedmiot | Testowanie i weryfikacja systemów sprzętowo-programowych - Przedmiot obieralny II | ||
| Specjalność | systemy komputerowe i technologie mobilne | ||
| Jednostka prowadząca | Katedra Architektury Komputerów i Telekomunikacji | ||
| Nauczyciel odpowiedzialny | Piotr Dziurzański <Piotr.Dziurzanski@zut.edu.pl> | ||
| Inni nauczyciele | |||
| ECTS (planowane) | 2,0 | ECTS (formy) | 2,0 |
| Forma zaliczenia | zaliczenie | Język | polski |
| Blok obieralny | 15 | Grupa obieralna | 3 |
Formy dydaktyczne
Wymagania wstępne
| KOD | Wymaganie wstępne |
|---|---|
| W-1 | Znajomość podstaw techniki cyfrowej |
Cele przedmiotu
| KOD | Cel modułu/przedmiotu |
|---|---|
| C-1 | Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych. |
Treści programowe z podziałem na formy zajęć
| KOD | Treść programowa | Godziny |
|---|---|---|
| laboratoria | ||
| T-L-1 | Zapoznanie ze standardem JTAG. | 2 |
| T-L-2 | Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG. | 4 |
| T-L-3 | Formalna weryfikacja w systemie NuSMV. | 1 |
| T-L-4 | Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL. | 1 |
| T-L-5 | Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL. | 1 |
| T-L-6 | Weryfikacja dynamiczna z wykorzystaniem biblioteki SCV. | 1 |
| 10 | ||
| wykłady | ||
| T-W-1 | Walidacja a weryfikacja. Podział weryfikacji. Pokrycie kodu a pokrycie funkcjonalności. Uzysk i przyczyny zmniejszenia uzysku. Miara i jednostka jakości procesu testowania. | 2 |
| T-W-2 | Kontrolowalność a obserwowalność. Ścieżka sterująca i typy SISO. Generatory wektorów testowych i sygnatury. Rodzaje rejestrów LFSR dla wielomianów prostych i odwrotnych. SISR a MISR. Tryby pracy BILBO. | 2 |
| T-W-3 | Porty i rejestry w JTAG. Cztery tryby pracy komórki brzegowej. Instrukcje obowiązkowe JTAG. Instrukcje opcjonalne JTAG. Język BSDL. Podstawowe cechy standardu IEEE 1500. | 1 |
| T-W-4 | Weryfikacja formalna. Logiki CTL, LTL i CTL*. Ograniczone sprawdzanie modeli. | 1 |
| T-W-5 | Problem SAT dla formuły CNF. Klasy algorytmów rozwiązujących SAT. Naiwne wyszukiwanie wsteczne. | 1 |
| T-W-6 | Warstwy w PSL. Operatory temporalne w PSL. Sugar Extended Regular Expressions (SEREs). | 2 |
| T-W-7 | Środowisko testowe na poziomie transakcyjnym. Introspekcja danych w SCV. Nagrywanie transakcji w SCV. Typy randomizacji w SCV. | 1 |
| 10 | ||
Obciążenie pracą studenta - formy aktywności
| KOD | Forma aktywności | Godziny |
|---|---|---|
| laboratoria | ||
| A-L-1 | uczestnictwo w zajęciach | 10 |
| A-L-2 | przygotowanie się do zajęć | 12 |
| 22 | ||
| wykłady | ||
| A-W-1 | uczestnictwo w zajęciach | 10 |
| A-W-2 | przygotowanie się do zajęć | 22 |
| 32 | ||
Metody nauczania / narzędzia dydaktyczne
| KOD | Metoda nauczania / narzędzie dydaktyczne |
|---|---|
| M-1 | Wykład informacyjny |
| M-2 | Wykład problemowy |
| M-3 | Metoda przypadków |
| M-4 | Ćwiczenia laboratoryjne |
Sposoby oceny
| KOD | Sposób oceny |
|---|---|
| S-1 | Ocena podsumowująca: egzamin pisemny |
| S-2 | Ocena podsumowująca: kolokwium pisemne |
Zamierzone efekty kształcenia - wiedza
| Zamierzone efekty kształcenia | Odniesienie do efektów kształcenia dla kierunku studiów | Odniesienie do efektów zdefiniowanych dla obszaru kształcenia | Cel przedmiotu | Treści programowe | Metody nauczania | Sposób oceny |
|---|---|---|---|---|---|---|
| I_2A_D18/O/3-1_W01 Zaawansowana znajomość standardu JTAG i jego modyfikacji | I_2A_W05 | — | C-1 | T-W-3, T-L-1, T-L-2 | M-2, M-1 | S-1 |
| I_2A_D18/O/3-1_W02 Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej | I_2A_W01 | — | C-1 | T-W-4, T-W-6, T-W-5, T-L-3, T-L-4, T-L-5 | M-2, M-1 | S-1 |
Zamierzone efekty kształcenia - umiejętności
| Zamierzone efekty kształcenia | Odniesienie do efektów kształcenia dla kierunku studiów | Odniesienie do efektów zdefiniowanych dla obszaru kształcenia | Cel przedmiotu | Treści programowe | Metody nauczania | Sposób oceny |
|---|---|---|---|---|---|---|
| I_2A_D18/O/3-1_U01 Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych | I_2A_U04, I_2A_U08 | — | C-1 | T-W-3, T-L-1, T-L-2 | M-4, M-3 | S-2 |
Kryterium oceny - wiedza
| Efekt kształcenia | Ocena | Kryterium oceny |
|---|---|---|
| I_2A_D18/O/3-1_W01 Zaawansowana znajomość standardu JTAG i jego modyfikacji | 2,0 | nie spełnia wymogów na ocenę 3,0. |
| 3,0 | zna budowę generatorów wektorów testowych i sygnatur, zna pojęcie rejestru LFSR, zna porty i rejestry JTAG oraz instrukcje obowiązkowe JTAG. | |
| 3,5 | jak na ocenę 3,0 oraz rozumie różnicę między SISR a MISR i zna tryby pracy obserwatora BILBO. | |
| 4,0 | jak na ocenę 3,5 oraz zna rodzaje rejestrów LFSR dla wielomianów prostych i odwrotnych, instrukcje opcjonalne JTAG oraz podstawy języka BSDL. Rozumie pojęcie introspekcji danych w SCV. | |
| 4,5 | jak na ocenę 4.0 oraz zna zaawansowane cechy języka BSDL, zna typy randomizacji w SCV. | |
| 5,0 | jak na ocenę 4,5 oraz zna podstawowe cechy standardu IEEE 1500. | |
| I_2A_D18/O/3-1_W02 Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej | 2,0 | nie spełnia wymogów na ocenę 3,0. |
| 3,0 | zna podstawy weryfikacji formalnej w logice CTL, rozumie kwantyfikatory ścieżek oraz operatory temporalne X, F, G i U. | |
| 3,5 | jak na ocenę 3,0 oraz rozumie pojęcie formuł sprawiedliwych. | |
| 4,0 | jak na ocenę 3,5 oraz zna różnicę między logiką CTL a LTL, zna pojęcie ograniczonego sprawdzania modeli. | |
| 4,5 | jak na ocenę 4,0 oraz zna podstawy języka PSL, w tym SERE. | |
| 5,0 | jak na ocenę 4,5 oraz zna klasy algorytmów rozwiązujących SAT, a także rozumie pojęcie naiwnego wyszukiwania wstecznego. |
Kryterium oceny - umiejętności
| Efekt kształcenia | Ocena | Kryterium oceny |
|---|---|---|
| I_2A_D18/O/3-1_U01 Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych | 2,0 | nie spełnia wymogów na ocenę 3,0. |
| 3,0 | potrafi dokonać testowania zewnętrznego z wykorzystaniem standardu JTAG, potrafi zapisać proste formuły w logice temporalnej CTL. | |
| 3,5 | jak na ocenę 3,0 oraz potrafi zaprojektować środowisko testwo z generatorem wektorów testowych i sygnatur, potrafi zapisać formuły sprawiedliwe. | |
| 4,0 | jak na ocenę 3,5 oraz potrafi wykorzystać język BSDL w procesie testowania, potrafi wykorzystywać instrukcje opcjonalne JTAG, potrafi dokonać introspekcji danych w SCV. | |
| 4,5 | jak na ocenę 4,0 oraz potrafi zapisać formuły w języku PSL (w tym SERE), potrafi wykorzystać różne cechy randomizacji w SCV. | |
| 5,0 | jak na ocenę 4,5 oraz potrafi zaplanować i przeprowadzić testowanie systemu sprzętowo-programowego z wykorzystaniem różnych technik statycznych i dynamicznych. |
Literatura podstawowa
- M. Fujita, I. Ghosh, M. Prasad, Verification Techniques For System-Level Design, MK, 2007
- E. Clarke et. al., Model Checking, MIT Press, 1999
- Kenneth P. Parker, The Boundary-scan Handbook, Springer, 2003
Literatura dodatkowa
- L. Singh, L. Drucker, N. Khan, Advanced Verification Techniques: A SystemC Based Approach for Successful Tapeout, Kluwer, 2004
- L.-T. Wang, C. E. Stroud, N. A. Touba, System-on-Chip Test Architectures, MK, 2007
- K. Sapiecha, Testowanie i diagnostyka systemów cyfrowych, WNT, 1987
- M. Zwoliński, Projektowanie układów cyfrowych z wykorzystaniem języka VHDL, WKiŁ, 2002
- C. Eisner, D. Fisman, A Practical Introduction to PSL, Springer, 2006