Zachodniopomorski Uniwersytet Technologiczny w Szczecinie

Wydział Informatyki - Informatyka (S2)

Sylabus przedmiotu Testowanie i weryfikacja systemów sprzętowo-programowych - Przedmiot obieralny II:

Informacje podstawowe

Kierunek studiów Informatyka
Forma studiów studia stacjonarne 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 14 Grupa obieralna 3

Formy dydaktyczne

Forma dydaktycznaKODSemestrGodzinyECTSWagaZaliczenie
laboratoriaL2 15 0,80,50zaliczenie
wykładyW2 15 1,20,50zaliczenie

Wymagania wstępne

KODWymaganie wstępne
W-1Znajomość podstaw techniki cyfrowej

Cele przedmiotu

KODCel modułu/przedmiotu
C-1Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.

Treści programowe z podziałem na formy zajęć

KODTreść programowaGodziny
laboratoria
T-L-1Zapoznanie ze standardem JTAG.2
T-L-2Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.5
T-L-3Formalna weryfikacja w systemie NuSMV.2
T-L-4Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL.2
T-L-5Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL.2
T-L-6Weryfikacja dynamiczna z wykorzystaniem biblioteki SCV.2
15
wykłady
T-W-1Walidacja 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-2Kontrolowalność 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-3Porty 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.3
T-W-4Weryfikacja formalna. Logiki CTL, LTL i CTL*. Ograniczone sprawdzanie modeli.2
T-W-5Problem SAT dla formuły CNF. Klasy algorytmów rozwiązujących SAT. Naiwne wyszukiwanie wsteczne.2
T-W-6Warstwy 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.2
15

Obciążenie pracą studenta - formy aktywności

KODForma aktywnościGodziny
laboratoria
A-L-1uczestnictwo w zajęciach15
A-L-2przygotowanie się do zajęć8
A-L-3Udzał w konsultacjach i zaliczeniu formy zajęć2
25
wykłady
A-W-1uczestnictwo w zajęciach15
A-W-2przygotowanie się do zajęć, lektura materiałów i podręczników15
A-W-3Udzał w konsultacjach i zaliczeniu formy zajęć2
32

Metody nauczania / narzędzia dydaktyczne

KODMetoda nauczania / narzędzie dydaktyczne
M-1Wykład informacyjny
M-2Wykład problemowy
M-3Metoda przypadków
M-4Ćwiczenia laboratoryjne

Sposoby oceny

KODSposób oceny
S-1Ocena podsumowująca: egzamin pisemny
S-2Ocena podsumowująca: kolokwium pisemne

Zamierzone efekty kształcenia - wiedza

Zamierzone efekty kształceniaOdniesienie do efektów kształcenia dla kierunku studiówOdniesienie do efektów zdefiniowanych dla obszaru kształceniaCel przedmiotuTreści programoweMetody nauczaniaSposób oceny
I_2A_D18/O5/2-3_W01
Zaawansowana znajomość standardu JTAG i jego modyfikacji
I_2A_W05C-1T-L-1, T-L-2, T-W-3M-1, M-2S-1
I_2A_D18/O5/2-3_W02
Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej
I_2A_W01C-1T-L-3, T-L-4, T-L-5, T-W-4, T-W-5, T-W-6M-1, M-2S-1

Zamierzone efekty kształcenia - umiejętności

Zamierzone efekty kształceniaOdniesienie do efektów kształcenia dla kierunku studiówOdniesienie do efektów zdefiniowanych dla obszaru kształceniaCel przedmiotuTreści programoweMetody nauczaniaSposób oceny
I_2A_D18/O5/2-3_U01
Potrafi przetestować funkcjonalnie system sprzętowy z wykorzystaniem zaawansowanych możliwości standardu JTAG.
I_2A_U08C-1T-L-1, T-L-2, T-W-3M-3, M-4S-2

Kryterium oceny - wiedza

Efekt kształceniaOcenaKryterium oceny
I_2A_D18/O5/2-3_W01
Zaawansowana znajomość standardu JTAG i jego modyfikacji
2,0nie spełnia wymogów na ocenę 3,0.
3,0zna budowę generatorów wektorów testowych i sygnatur, zna pojęcie rejestru LFSR, zna porty i rejestry JTAG oraz instrukcje obowiązkowe JTAG.
3,5jak na ocenę 3,0 oraz rozumie różnicę między SISR a MISR i zna tryby pracy obserwatora BILBO.
4,0jak 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,5jak na ocenę 4.0 oraz zna zaawansowane cechy języka BSDL, zna typy randomizacji w SCV.
5,0jak na ocenę 4,5 oraz zna podstawowe cechy standardu IEEE 1500.
I_2A_D18/O5/2-3_W02
Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej
2,0nie spełnia wymogów na ocenę 3,0.
3,0zna podstawy weryfikacji formalnej w logice CTL, rozumie kwantyfikatory ścieżek oraz operatory temporalne X, F, G i U.
3,5jak na ocenę 3,0 oraz rozumie pojęcie formuł sprawiedliwych.
4,0jak na ocenę 3,5 oraz zna różnicę między logiką CTL a LTL, zna pojęcie ograniczonego sprawdzania modeli.
4,5jak na ocenę 4,0 oraz zna podstawy języka PSL, w tym SERE.
5,0jak 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łceniaOcenaKryterium oceny
I_2A_D18/O5/2-3_U01
Potrafi przetestować funkcjonalnie system sprzętowy z wykorzystaniem zaawansowanych możliwości standardu JTAG.
2,0nie spełnia wymogów na ocenę 3,0.
3,0potrafi dokonać testowania zewnętrznego z wykorzystaniem standardu JTAG, potrafi zapisać proste formuły w logice temporalnej CTL.
3,5jak na ocenę 3,0 oraz potrafi zaprojektować środowisko testwo z generatorem wektorów testowych i sygnatur, potrafi zapisać formuły sprawiedliwe.
4,0jak 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,5jak 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,0jak na ocenę 4,5 oraz potrafi zaplanować i przeprowadzić testowanie systemu sprzętowo-programowego z wykorzystaniem różnych technik statycznych i dynamicznych.

Literatura podstawowa

  1. M. Fujita, I. Ghosh, M. Prasad, Verification Techniques For System-Level Design, MK, 2007
  2. E. Clarke et. al., Model Checking, MIT Press, 1999
  3. Kenneth P. Parker, The Boundary-scan Handbook, Springer, 2003

Literatura dodatkowa

  1. L. Singh, L. Drucker, N. Khan, Advanced Verification Techniques: A SystemC Based Approach for Successful Tapeout, Kluwer, 2004
  2. L.-T. Wang, C. E. Stroud, N. A. Touba, System-on-Chip Test Architectures, MK, 2007
  3. K. Sapiecha, Testowanie i diagnostyka systemów cyfrowych, WNT, 1987
  4. M. Zwoliński, Projektowanie układów cyfrowych z wykorzystaniem języka VHDL, WKiŁ, 2002
  5. C. Eisner, D. Fisman, A Practical Introduction to PSL, Springer, 2006

Treści programowe - laboratoria

KODTreść programowaGodziny
T-L-1Zapoznanie ze standardem JTAG.2
T-L-2Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.5
T-L-3Formalna weryfikacja w systemie NuSMV.2
T-L-4Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL.2
T-L-5Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL.2
T-L-6Weryfikacja dynamiczna z wykorzystaniem biblioteki SCV.2
15

Treści programowe - wykłady

KODTreść programowaGodziny
T-W-1Walidacja 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-2Kontrolowalność 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-3Porty 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.3
T-W-4Weryfikacja formalna. Logiki CTL, LTL i CTL*. Ograniczone sprawdzanie modeli.2
T-W-5Problem SAT dla formuły CNF. Klasy algorytmów rozwiązujących SAT. Naiwne wyszukiwanie wsteczne.2
T-W-6Warstwy 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.2
15

Formy aktywności - laboratoria

KODForma aktywnościGodziny
A-L-1uczestnictwo w zajęciach15
A-L-2przygotowanie się do zajęć8
A-L-3Udzał w konsultacjach i zaliczeniu formy zajęć2
25
(*) 1 punkt ECTS, odpowiada około 30 godzinom aktywności studenta

Formy aktywności - wykłady

KODForma aktywnościGodziny
A-W-1uczestnictwo w zajęciach15
A-W-2przygotowanie się do zajęć, lektura materiałów i podręczników15
A-W-3Udzał w konsultacjach i zaliczeniu formy zajęć2
32
(*) 1 punkt ECTS, odpowiada około 30 godzinom aktywności studenta
PoleKODZnaczenie kodu
Zamierzone efekty kształceniaI_2A_D18/O5/2-3_W01Zaawansowana znajomość standardu JTAG i jego modyfikacji
Odniesienie do efektów kształcenia dla kierunku studiówI_2A_W05Ma rozszerzoną i podbudowaną teoretycznie wiedzę z zakresu metod informatyki wykorzystywanych do rozwiązywania problemów w wybranych obszarach nauki i techniki
Cel przedmiotuC-1Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programoweT-L-1Zapoznanie ze standardem JTAG.
T-L-2Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.
T-W-3Porty 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.
Metody nauczaniaM-1Wykład informacyjny
M-2Wykład problemowy
Sposób ocenyS-1Ocena podsumowująca: egzamin pisemny
Kryteria ocenyOcenaKryterium oceny
2,0nie spełnia wymogów na ocenę 3,0.
3,0zna budowę generatorów wektorów testowych i sygnatur, zna pojęcie rejestru LFSR, zna porty i rejestry JTAG oraz instrukcje obowiązkowe JTAG.
3,5jak na ocenę 3,0 oraz rozumie różnicę między SISR a MISR i zna tryby pracy obserwatora BILBO.
4,0jak 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,5jak na ocenę 4.0 oraz zna zaawansowane cechy języka BSDL, zna typy randomizacji w SCV.
5,0jak na ocenę 4,5 oraz zna podstawowe cechy standardu IEEE 1500.
PoleKODZnaczenie kodu
Zamierzone efekty kształceniaI_2A_D18/O5/2-3_W02Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej
Odniesienie do efektów kształcenia dla kierunku studiówI_2A_W01Ma poszerzoną i pogłębioną wiedzę w zakresie wybranych działów matematyki teoretycznej oraz matematyki stosowanej
Cel przedmiotuC-1Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programoweT-L-3Formalna weryfikacja w systemie NuSMV.
T-L-4Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL.
T-L-5Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL.
T-W-4Weryfikacja formalna. Logiki CTL, LTL i CTL*. Ograniczone sprawdzanie modeli.
T-W-5Problem SAT dla formuły CNF. Klasy algorytmów rozwiązujących SAT. Naiwne wyszukiwanie wsteczne.
T-W-6Warstwy w PSL. Operatory temporalne w PSL. Sugar Extended Regular Expressions (SEREs).
Metody nauczaniaM-1Wykład informacyjny
M-2Wykład problemowy
Sposób ocenyS-1Ocena podsumowująca: egzamin pisemny
Kryteria ocenyOcenaKryterium oceny
2,0nie spełnia wymogów na ocenę 3,0.
3,0zna podstawy weryfikacji formalnej w logice CTL, rozumie kwantyfikatory ścieżek oraz operatory temporalne X, F, G i U.
3,5jak na ocenę 3,0 oraz rozumie pojęcie formuł sprawiedliwych.
4,0jak na ocenę 3,5 oraz zna różnicę między logiką CTL a LTL, zna pojęcie ograniczonego sprawdzania modeli.
4,5jak na ocenę 4,0 oraz zna podstawy języka PSL, w tym SERE.
5,0jak na ocenę 4,5 oraz zna klasy algorytmów rozwiązujących SAT, a także rozumie pojęcie naiwnego wyszukiwania wstecznego.
PoleKODZnaczenie kodu
Zamierzone efekty kształceniaI_2A_D18/O5/2-3_U01Potrafi przetestować funkcjonalnie system sprzętowy z wykorzystaniem zaawansowanych możliwości standardu JTAG.
Odniesienie do efektów kształcenia dla kierunku studiówI_2A_U08Potrafi wykorzystywać narzędzia sprzętowo-programowe wspomagające rozwiązywanie wybranych problemów w różnych obszarach nauki i techniki
Cel przedmiotuC-1Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programoweT-L-1Zapoznanie ze standardem JTAG.
T-L-2Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.
T-W-3Porty 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.
Metody nauczaniaM-3Metoda przypadków
M-4Ćwiczenia laboratoryjne
Sposób ocenyS-2Ocena podsumowująca: kolokwium pisemne
Kryteria ocenyOcenaKryterium oceny
2,0nie spełnia wymogów na ocenę 3,0.
3,0potrafi dokonać testowania zewnętrznego z wykorzystaniem standardu JTAG, potrafi zapisać proste formuły w logice temporalnej CTL.
3,5jak na ocenę 3,0 oraz potrafi zaprojektować środowisko testwo z generatorem wektorów testowych i sygnatur, potrafi zapisać formuły sprawiedliwe.
4,0jak 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,5jak 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,0jak na ocenę 4,5 oraz potrafi zaplanować i przeprowadzić testowanie systemu sprzętowo-programowego z wykorzystaniem różnych technik statycznych i dynamicznych.