Zachodniopomorski Uniwersytet Technologiczny w Szczecinie

Wydział Informatyki - Informatyka (S1)

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

Informacje podstawowe

Kierunek studiów Informatyka
Forma studiów studia stacjonarne Poziom pierwszego stopnia
Tytuł zawodowy absolwenta inżynier
Obszary studiów nauki techniczne, studia inżynierskie
Profil ogólnoakademicki
Moduł
Przedmiot Testowanie i weryfikacja systemów sprzętowo-programowych
Specjalność systemy komputerowe i oprogramowanie
Jednostka prowadząca Katedra Architektury Komputerów i Telekomunikacji
Nauczyciel odpowiedzialny Piotr Dziurzański <Piotr.Dziurzanski@zut.edu.pl>
Inni nauczyciele
ECTS (planowane) 3,0 ECTS (formy) 3,0
Forma zaliczenia zaliczenie Język polski
Blok obieralny 10 Grupa obieralna 4

Formy dydaktyczne

Forma dydaktycznaKODSemestrGodzinyECTSWagaZaliczenie
laboratoriaL7 15 1,50,38zaliczenie
wykładyW7 15 1,50,62zaliczenie

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ęć20
A-L-3Udział w zaliczeniu i konsultacjach2
A-L-4Przygotowanie sprawozdań7
44
wykłady
A-W-1uczestnictwo w zajęciach15
A-W-2przygotowanie się do zajęć22
A-W-3Udział w zaliczeniu i konsultacjach2
A-W-4Przygotowanie się do zaliczenia wykładu5
44

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: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym

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łceniaOdniesienie do efektów kształcenia prowadzących do uzyskania tytułu zawodowego inżynieraCel przedmiotuTreści programoweMetody nauczaniaSposób oceny
I_1A_O4/10_W01
Znajomość testowania dynamicznego systemów sprzętowo-programowych oraz standardu JTAG
I_1A_W03C-1T-L-1, T-L-2, T-W-3M-1, M-2, M-3, M-4S-1
I_1A_O4/10_W02
Znajomość podstaw teoretycznych weryfikacji formalnej
I_1A_W01C-1T-L-4, T-L-5, T-L-6, T-L-3, T-W-4, T-W-5, T-W-6, T-W-7M-1, M-2, M-3, M-4S-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łceniaOdniesienie do efektów kształcenia prowadzących do uzyskania tytułu zawodowego inżynieraCel przedmiotuTreści programoweMetody nauczaniaSposób oceny
I_1A_O4/10_U01
Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych
I_1A_U01, I_1A_U02, I_1A_U04, I_1A_U18C-1T-L-1, T-L-2, T-W-3M-1, M-2, M-3, M-4S-1

Kryterium oceny - wiedza

Efekt kształceniaOcenaKryterium oceny
I_1A_O4/10_W01
Znajomość testowania dynamicznego systemów sprzętowo-programowych oraz standardu JTAG
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_1A_O4/10_W02
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_1A_O4/10_U01
Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych
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ęć20
A-L-3Udział w zaliczeniu i konsultacjach2
A-L-4Przygotowanie sprawozdań7
44
(*) 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ęć22
A-W-3Udział w zaliczeniu i konsultacjach2
A-W-4Przygotowanie się do zaliczenia wykładu5
44
(*) 1 punkt ECTS, odpowiada około 30 godzinom aktywności studenta
PoleKODZnaczenie kodu
Zamierzone efekty kształceniaI_1A_O4/10_W01Znajomość testowania dynamicznego systemów sprzętowo-programowych oraz standardu JTAG
Odniesienie do efektów kształcenia dla kierunku studiówI_1A_W03zna podstawy elektroniki, techniki analogowej i cyfrowej, ze szczególnym uwzględnieniem ich stosowanych aspektów, niezbędne do opisu i analizy działania systemów elektronicznych, w tym systemów zawierających układy programowalne
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
M-3Metoda przypadków
M-4Ćwiczenia laboratoryjne
Sposób ocenyS-1Ocena podsumowująca: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym
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_1A_O4/10_W02Znajomość podstaw teoretycznych weryfikacji formalnej
Odniesienie do efektów kształcenia dla kierunku studiówI_1A_W01ma wiedzę z matematyki teoretycznej ze szczególnym uwzględnieniem jej stosowanych aspektów, matematyki dyskretnej 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-4Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL.
T-L-5Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL.
T-L-6Weryfikacja dynamiczna z wykorzystaniem biblioteki SCV.
T-L-3Formalna weryfikacja w systemie NuSMV.
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).
T-W-7Środowisko testowe na poziomie transakcyjnym. Introspekcja danych w SCV. Nagrywanie transakcji w SCV. Typy randomizacji w SCV.
Metody nauczaniaM-1Wykład informacyjny
M-2Wykład problemowy
M-3Metoda przypadków
M-4Ćwiczenia laboratoryjne
Sposób ocenyS-1Ocena podsumowująca: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym
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_1A_O4/10_U01Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych
Odniesienie do efektów kształcenia dla kierunku studiówI_1A_U01potrafi w zakresie podstawowym projektować, implementować i testować oprogramowanie
I_1A_U02potrafi aktywnie uczestniczyć w pracach projektowych zespołowych i indywidualnych
I_1A_U04ma podstawowe umiejętności w zakresie programowania i podnoszenia niezawodności systemów wbudowanych
I_1A_U18umie opisywać i analizować działanie prostych systemów elektronicznych, w tym systemów zawierających układy programowalne
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
M-3Metoda przypadków
M-4Ćwiczenia laboratoryjne
Sposób ocenyS-1Ocena podsumowująca: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym
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.