Weryfikacja Systemów Cyfrowych

Cheatsheet Content

### Weryfikacja - Wprowadzenie Weryfikacja systemów cyfrowych to **sprawdzanie, czy implementacja projektu jest zgodna ze specyfikacją na wszystkich poziomach abstrakcji.** **Dlaczego weryfikować?** - Bezpieczeństwo i niezawodność. - Ograniczenie strat z błędów. - Weryfikacja to nawet **70% czasu projektowania**. - Inżynierowie skupiają się na typowych przypadkach, weryfikacja musi uwzględniać **wszystkie**. - Wzrost złożoności systemów i liczby układów cyfrowych. - Błędy na różnych poziomach: implementacji (projektant), syntezy (narzędzia), technologii, oprogramowania. **Co to jest błąd?** - Niezgodność implementacji ze specyfikacją. - Coś, na co klient będzie narzekał. **Przykłady błędów implementacji CPU:** - **Intel Pentium FDIV (1994):** błąd jednostki zmiennoprzecinkowej. - **Intel Meltdown (od 1995):** błąd tabeli stron prowadzący do wycieku danych. **Rodzaje weryfikacji:** - **Funkcjonalna:** Czy działa zgodnie z założeniami. - **Czasowa:** Czy spełnia wymogi czasowe. - **Topologiczna:** Dotycząca ułożenia elementów. - **Elektryczna:** Dotycząca parametrów elektrycznych. ### Podejścia do Weryfikacji 1. **Prototyp w technologii docelowej:** - Drogi i czasochłonny dla dużych projektów. - Niezbędny dla niektórych układów analogowych/mieszanych. 2. **Prototyp na FPGA:** - Możliwy dla dużych projektów dzięki pojemności FPGA. - Interakcja ze światem rzeczywistym, pomaga unikać błędów specyfikacji. - Mniej sterowalny niż symulacja. 3. **Symulacja:** - Podstawowe podejście dla układów cyfrowych wysokiej skali integracji. - Wymaga dużych zasobów obliczeniowych. 4. **Weryfikacja formalna:** - Dowód, że projekt spełnia specyfikację. - Zyskuje na popularności, ale wciąż niepraktyczna dla kompletnych projektów. ### Poziomy Abstrakcji (Diagram Y Gajskiego-Kuhna) - **Poziom systemu:** Definiowanie fragmentów systemu, komunikacji, interfejsów (np. CPU, GPU, pamięć). - **Poziom algorytmu:** Zachowanie podsystemów opisane w językach wysokopoziomowych (C/C++). - **Poziom transferów między rejestrami (RTL):** Opis transferów danych i czasu ich przesyłania między prostymi jednostkami funkcjonalnymi. - **Poziom bramek:** Funkcje cyfrowe reprezentowane przez połączone bramki logiczne. - **Poziom obwodu:** Funkcjonalność bramki realizowana przez połączenie tranzystorów (np. standardowa komórka). ### Weryfikacja - Metodologia **Cel:** Sprawdzenie, czy intencje projektanta są zgodne z zachowaniem systemu. **Algorytm weryfikacji funkcjonalnej (symulacja):** 1. **Plan weryfikacji:** Zestaw zadań potwierdzających poprawność działania (np. czy sumator poprawnie liczy bit przeniesienia). 2. **Środowisko testowe (testbench):** Sekwencja testowa na wejściach i obserwacja wyjść. 3. **Zakończenie weryfikacji:** Określenie, czy pokrycie funkcjonalne jest wystarczające (czy wszystkie funkcje zostały przetestowane). **Pokrycie projektu w symulacji:** - **Pokrycie funkcjonalne:** Jaka część funkcji projektu została sprawdzona. - **Pokrycie kodu:** Jaka część kodu źródłowego została sprawdzona. - **Pokrycie zdarzeń:** Liczba wyzwalanych zdarzeń. - **Pokrycie ścieżki:** Liczba wykonanych ścieżek dojścia do fragmentu kodu. - **Pokrycie strukturalne:** Sprawdzenie przypadków szczególnych (np. pusty/pełny bufor FIFO). - **Pokrycie warunków:** Sprawdzone permutacje wyrażeń Boolowskich. - **Pokrycie stanów:** Osiągnięte stany automatu i przejścia między nimi. - **Pokrycie rozgałęzień:** Spełnione warunki w `case` i `if..else`. - **Pokrycie asercji:** Ile razy asercja została sprawdzona. **100% pokrycia kodu nie oznacza wykrycia wszystkich błędów!** Błędy mogą ujawnić się po nietypowych danych wejściowych. ### Weryfikacja Formalna **Definicja:** Użycie narzędzi, które matematycznie analizują przestrzeń możliwych zachowań projektu. **Cechy:** - Dowód poprawności, nie tylko sprawdzenie, czy działa. - Może być kompletna (100% pokrycia funkcjonalnego). - Zwykle uzupełnia symulacje. **Rodzaje weryfikacji formalnej:** 1. **Sprawdzanie równoważności:** - Porównywanie, czy dwa opisy obwodów mają takie samo zachowanie (np. RTL vs. bramki). - **BDD (Binarne Diagramy Decyzyjne):** Grafy reprezentujące funkcje Boolowskie. ROBDD (Reduced Ordered BDD) to forma kanoniczna. Dwie funkcje są równoważne, jeśli ich ROBDD są takie same. - **SAT (Boolean Satisfiability Problem):** Znalezienie przypisania wartości zmiennych, dla których funkcja Boolowska jest prawdziwa. Używane do sprawdzania równoważności poprzez konstrukcję obwodu "Miter" (XOR wyjść) – jeśli Miter jest niespełnialny, obwody są równoważne. - **AIG (And/Inverter Graph):** Kierunkowy graf reprezentujący implementację funkcji logicznej. Węzły to bramki AND, krawędzie mogą być negowane. AIG są mniejsze niż BDD, ale niekanoniczne. Redukcja (przez SAT lub BDD) i mieszanie (strashing) mogą doprowadzić do postaci kanonicznej. - **Układy sekwencyjne:** Można sprowadzić do postaci kombinacyjnej (pomijając zagadnienia czasowe) lub wykonać pełną weryfikację sekwencyjną opartą na przejściach między stanami. 2. **Sprawdzanie modelu (Model Checking):** - Automatyczna technika weryfikacji. - Wymaga: modelu systemu i formuły logicznej opisującej właściwości. - Algorytm sprawdza, czy model spełnia formułę. Jeśli nie, podaje kontrprzykład. - Stosowane do układów sekwencyjnych i protokołów komunikacyjnych. - **Specyfikacja:** Logika temporalna (LTL, CTL) – pozwala wnioskować z uwzględnieniem czasu. - **Model:** Struktura Kripke'go – model stanów i przejść. - **Procedura:** Model systemu M (automat Kripke'go) przekształcany do automatu Büchi'ego BM. Negacja własności φ (⌐φ) przekształcana do automatu Büchi'ego B⌐φ. Model jest zgodny ze specyfikacją, jeśli język automatu wynikowego L(BM × B⌐φ) jest pusty. 3. **Dowodzenie twierdzeń:** - Poszukiwanie dowodu poprawności implementacji w oparciu o specyfikację. - Stosowane dla systemów krytycznych (medyczne, awionika) i bardzo złożonych (FPU). - Może być automatyczne (dla typowych problemów) lub interaktywne (wymaga udziału człowieka). - Wymaga opisu sprzętu i specyfikacji w języku logiki wyższego rzędu (HOL – Higher Order Logic). 4. **Symulacje symboliczne:** - Tworzenie wyrażeń zamiast wartości bitów jako wynik symulacji. - Operuje na przekształceniach funkcji Boolowskich, upraszczając je. - Wejścia mogą być symbolami (wolne zmienne) lub wyrażeniami. - Pozwala symulować wiele zbiorów wektorów wejściowych jednocześnie. - Może analizować układy sekwencyjne ze sprzężeniem zwrotnym. ### Symulacje **Rodzaje:** 1. **Symulacje logiczne oparte na zdarzeniach:** - Działanie symulatora po każdym zdarzeniu propagowanym. - Dokładne, ale powolne dla dużych projektów. 2. **Symulacje logiczne oparte na cyklach:** - Nie mają pojęcia czasu w cyklu zegara, oceniają logikę raz na cykl. - Szybsze (5-100x) niż zdarzeniowe, ale mogą prowadzić do błędów symulacji. - Tylko dla logiki synchronicznej. 3. **Emulacje sprzętowe:** - Testowanie na sprzętowym modelu opartym na FPGA. - Kilkaset-kilka tysięcy razy szybsze niż symulacje software'owe. - Wady: długi czas kompilacji, ograniczona ilość danych wyjściowych, utrudnione debugowanie. 4. **Symulacje losowe:** - Szybkie, ale dają małe pokrycie. - Używane do sprawdzania równoważności par węzłów. 5. **Symulacje kompletne:** - Wymagają sprawdzenia wszystkich kombinacji wejść. - Bardzo czasochłonne dla większych układów (np. 32-bitowy komparator: 583 460 lat). - Dają 100% pokrycie funkcjonalne dla układów kombinacyjnych. **Sposoby tworzenia wektorów testujących:** - **Ukierunkowany:** Ręczny test danej funkcji, gwarantuje pokrycie, ale pracochłonny. - **Losowy:** Generowane przez maszynę, znajduje przypadki nieuwzględnione przez projektantów, ale marnuje czas na nieciekawe przypadki. - **Ograniczony losowy:** Losowe dane, ale ukierunkowane, szybko generuje ciekawe przypadki, ale trudno trafić we wszystkie. **Asercje:** - Predykaty umieszczone w kodzie opisu sprzętu, opisujące oczekiwane zachowanie. - Pomagają zwiększyć obserwowalność i sterowność projektu. - Typy: Funkcjonalne (np. FIFO nie przepełnia się), jakościowe (np. wszystkie przerzutniki resetowalne). - **ABV (Assertion-Based Verification):** Metoda weryfikacji oparta na asercjach. - **Techniki ABV:** - **Dynamiczna:** Weryfikacja podczas symulacji. - **Statyczna:** Wyczerpujące sprawdzanie własności (Model Checking). - **Kto tworzy asercje?** Projektant (przejścia stanów), inżynier weryfikujący (interfejs), konstruktor urządzenia (strukturalne, niezmienniki). - **Języki obsługujące asercje:** VHDL (`assert`), OVL, PSL, OVA, SVA (SystemVerilog Assertion), HVL. ### Testowanie Wytworzonego Układu **Typowe usterki:** - **Stały stan węzła (stuck-at):** Linia trwale ustawiona na 0 (s-a-0) lub 1 (s-a-1). - **Usterki typu mostek (zwarcie) / przerwa w ścieżkach.** - **Tranzystor CMOS ze stałym stanem:** Zablokowany (przewodzi/nie) lub trwale otwarty. - **Błędy i różnice w opóźnieniach/czasie propagacji.** - **Błędy funkcjonalne.** **Metody testowania:** 1. **JTAG (IEEE Std 1149.1):** Standard obejmujący interfejs i instrukcje do programowania, debugowania i testowania układów. Wykorzystuje koncepcję Boundary-Scan (skanowanie graniczne). 2. **BIST (Built-In Self-Test):** Samotestowanie układu za pomocą wbudowanego modułu. - **MBIST:** Dla pamięci, generuje wzorce i odczytuje w celu wykrycia defektów, może naprawiać. - **LBIST:** Dla układów logicznych, używa generatora wzorców pseudolosowych, kompresuje wyniki do sygnatury. - Wady: wydłuża czas projektowania, zwiększa powierzchnię i zużycie energii. 3. **ATPG (Automatic Test-Pattern Generation):** Metoda generacji wektorów testowych do wykrywania ściśle określonych błędów. - **Metody kombinacyjne:** Oparte na tablicy prawdy, równaniach Boolowskich, analizie strukturalnej (np. Algorytm D, PODEM, FAN). - **Metody sekwencyjne:** Oparte na rozwinięciu kombinacyjnym. - **Etapy:** Aktywacja błędu, propagacja błędu, uzasadnienie linii. ### VHDL i Verilog - Porównanie **VHDL (Very High Speed Integrated Circuits Hardware Description Language):** - Opracowany przez Departament Obrony USA (1981), standard IEEE (1987). - Podejście top-down. - Sekcje: Entity (interfejs), Architecture (zachowanie), Configuration, Package. - Podobny do ADA, "trudniejszy" do nauki. **Verilog:** - Opracowany przez Gateway Design Automation (1980), standard IEEE (1995). - Jeden blok konstrukcyjny: Module (może być behawioralny lub strukturalny). - Podobny do C, "łatwiejszy" do nauki. **Podobieństwa:** - Wprowadziły wyższy poziom abstrakcji w projektowaniu. - Symulacja i synteza to główne narzędzia. **Różnice:** - **Poziomy abstrakcji:** Verilog (klucze, bramki, strukturalny, rejestry, RTL, behawioralny), VHDL (abstrakcyjny behawioralny). - **Składnia:** VHDL (silnie typowany), Verilog (luźniej typowany, rozróżnia małe/DUŻE litery). - **Przypisania:** - **VHDL:** `signal ### SystemVerilog Rozszerzenie standardu Verilog (IEEE SystemVerilog2005). **Kluczowe cechy:** - **Programowanie obiektowe (OOP):** Klasy, dziedziczenie, polimorfizm. - `class C { int x; task set (int i) {x=i;} function int get {return x;} }`. - `local`/`protected` dla zasięgu zmiennych. - **Modelowanie 2-stanowe:** Typy danych `bit`, `byte`, `shortint`, `int`, `longint` (w przeciwieństwie do 4-stanowego `reg`/`logic` z `X`/`Z`). - **Tablice:** - **Dynamicznie alokowane:** Rozmiar ustalany/zmieniany w trakcie (`new[]`, `size()`, `delete()`). - **Statyczne:** Jedno- i wielowymiarowe. - **Asocjacyjne:** Indeksowane dowolnym typem, alokują pamięć tylko gdy używane (`num()`, `delete()`, `exists()`, `first()`, `last()`, `next()`, `prev()`). - **Kolejki (`queues`):** Zmienne, uporządkowane zbiory elementów, dynamiczny rozmiar (`size()`, `insert()`, `delete()`, `push_front()`, `push_back()`, `pop_front()`, `pop_back()`). - **Przekazywanie wartości przez referencje:** Podprogramy mogą odnosić się bezpośrednio do argumentów (`ref int i`). - **Mailbox:** Mechanizm komunikacji między procesami, przechowuje wiadomości tymczasowo (`new()`, `try_put()`, `get()`, `try_get()`, `num()`). - **Asercje:** Podobnie jak w Verilog, ale rozszerzone. - **Natychmiastowe:** Sprawdzają stan w bieżącym czasie symulacji (`assert (warunek)`). - **Współbieżne:** Sprawdzają kolejność zdarzeń rozłożonych na wiele cykli zegara (`assert property (@(posedge clk) ...)`). Używają `sequence` i `property`. - **Blok `program`:** Zawiera kompletne środowisko testowe, oddziela środowisko od projektu. - **Blok zegarowy (`clocking`):** Zestaw sygnałów zsynchronizowanych z określonym zegarem, rozwiązuje problemy synchronizacji w testbenchu. - **Kontrola procesu (`process`):** Wbudowana klasa do kontroli procesów/wątków (`self()`, `status()`, `kill()`, `await()`, `suspend()`, `resume()`). - **Semafory (`semaphore`):** Wbudowana klasa do kontroli dostępu do współdzielonych zasobów (`new()`, `get()`, `put()`, `try_get()`). - **Ograniczone wartości losowe:** Generowanie pseudolosowych liczb (`$urandom()`, `$urandom_range()`). - **Pokrycie funkcjonalne:** Wbudowane metody do analizy pokrycia (zmiennych, wyrażeń, zależności). - **Interfejsy:** Hermetyzują komunikację między blokami, ułatwiają ponowne użycie, mogą zawierać parametry, zmienne, funkcje, zadania. - **Zagnieżdżanie modułów:** Deklaracja modułu w ramach innego modułu. - **Nieograniczone porty:** Porty mogą być deklarowane jako `logic`, SystemVerilog sam dobiera `wire` lub `reg`. - **Słowa kluczowe `unique`/`priority`:** Używane z `if/else` i `case` do unikania błędów syntezy (np. zatrzasków). **Środowisko testowe SystemVerilog:** - **Generator:** Generuje sekwencje testowe (losowe wartości). - **Sterownik (Driver):** Odbiera wzbudzenia z generatora i steruje DUT. - **Monitor:** Próbkuje sygnały interfejsu i przekształca je na transakcje. - **Tablica wyników (Scoreboard):** Odbiera transakcje z monitora i porównuje z oczekiwanymi wartościami. - **Agent:** Grupuje generator, sterownik i monitor. - **Środowisko (Environment):** Zawiera wszystkie elementy testbenchu. - **Transakcja:** Klasa zawierająca dane do wzbudzenia DUT. ### OVL (Open Verification Libraries) **Definicja:** Biblioteki typu open-source, pozwalające na implementację weryfikacji opartej na asercjach w językach opisu sprzętu. **Korzyści:** - Sprawdzone i sparametryzowane zestawy asercji. - Ukrywają i narzucają metodologię. - Minimalizują potrzebę ekspertów języka asercji. - Zwiększają obserwowalność projektu. - Upraszczają diagnostykę błędów. - Umożliwiają ponowne użycie asercji dla różnych metodologii (symulacja, weryfikacja formalna). **Użytkowanie:** - Umieszczanie modułów sprawdzających (checkers) obok modułów projektu. - Checkers są powiązane z sygnałami obwodów przez porty. - Funkcjonalność checkers można modyfikować przez parametry. - Checkers mogą służyć do sprawdzania asercji, założeń lub punktów pokrycia. **Konfiguracja modułów sprawdzających:** - **Właściwości:** Atrybuty projektowe weryfikowane przez asercję (kombinacyjne, czasowe). - **Komunikat (`msg`):** Łańcuch znakowy wyświetlany w przypadku błędu. - **Istotność (`severity`):** `OVL_FATAL`, `OVL_ERROR`, `OVL_WARNING`, `OVL_INFO`. - **Typ właściwości (`property_type`):** Określa, czy sprawdzać asercje/założenia i czy uwzględniać wartości X/Z. Np. `OVL_ASSERT`, `OVL_ASSUME`, `OVL_ASSERT_2STATE`, `OVL_IGNORE`. - **Poziom pokrycia (`cover_level`):** Określa raportowane informacje o pokryciu. Np. `OVL_COVER_SANITY`, `OVL_COVER_BASIC`, `OVL_COVER_CORNER`, `OVL_COVER_STATISTIC`, `OVL_COVER_NONE`, `OVL_COVER_ALL`. **Przykładowe moduły sprawdzające:** - `ovl_always`: Sprawdza, czy wyrażenie jest zawsze prawdziwe. - `ovl_never`: Sprawdza, czy wyrażenie nigdy nie jest prawdziwe. - `ovl_cycle_sequence`: Sprawdza, czy po warunku następuje sekwencja zdarzeń. - `ovl_implication`: Sprawdza, czy z jednego wyrażenia wynika drugie. - `ovl_never_unknown`: Sprawdza, czy wyrażenie nie zawiera `X`/`Z`. - `ovl_next`: Sprawdza, czy wyrażenie jest prawdziwe po określonej liczbie cykli. - `ovl_one_hot`: Sprawdza, czy w słowie jest dokładnie jeden bit ustawiony na `1`. - `ovl_zero_one_hot`: Sprawdza, czy w słowie jest zero lub jeden bit ustawiony na `1`. - `ovl_range`: Sprawdza, czy wyrażenie mieści się w zakresie. ### OVM (Open Verification Methodology) **Definicja:** Biblioteka open-source klasy podstawowej napisana w SystemVerilog. Implementuje środowisko weryfikacyjne i funkcje pobudzeń. **Historia:** Opracowana przez Mentor Graphics i Cadence (2008), stała się podstawą UVM. **Podstawy:** - Metodologia weryfikacji funkcjonalnej w SystemVerilog. - Przenośny kod do stosowania we wszystkich symulatorach zgodnych z SystemVerilog. - Oparty na symulacji, ale może być używany z asercjami, akceleracją sprzętową. - Opis DUT może być w Verilog, SystemVerilog, VHDL, SystemC. **Testbench OVM:** - Pełne środowiska weryfikacyjne złożone z komponentów wielokrotnego użytku. - Oparte na ograniczonej losowej symulacji i pokryciu. - **Koncepcja wielokrotnego użytku:** Jedno środowisko dla wielu testów. **Struktura testbencha OVM (warstwowa):** - **DUT (Device Under Test):** Najniższa warstwa, opisana na dowolnym poziomie abstrakcji. - **Warstwa transaktorów:** Konwertuje sygnały między poziomem transakcji a poziomem wyprowadzeń DUT. - **Monitor:** Monitoruje wyprowadzenia, konwertuje zmiany wartości na strumień transakcji (pasywny). - **Sterownik (Driver):** Konwertuje strumień transakcji na aktywność na poziomie pinów. - **Responder:** Reaguje na aktywność na wyprowadzeniach. - **Komponenty operacyjne (powyżej transaktorów):** Generują aktywność DUT (na poziomie transakcji). - **Generatory wzbudzeń testowych:** Generują strumień transakcji (losowe, ukierunkowane). - **Moduł niezależny (Master):** Dwukierunkowy, wysyła żądania, otrzymuje odpowiedzi. - **Moduł zależny (Slave):** Dwukierunkowy, odpowiada na zapytania. - **Komponenty analizujące:** Odbierają informacje, aby określić poprawność/kompletność testu. - **Tablice wyników (Scoreboards):** Określają poprawność testu. - **Analizatory pokrycia:** Ustalają kompletność weryfikacji. - **Kontroler:** Główny wątek testu, zarządza aktywnością weryfikacji. **Wymiana danych (TLM - Transaction-Level Modeling):** - Komponenty komunikują się, przesyłając transakcje. - **Transakcja:** Ograniczona czasowo kwantowa aktywność. **Komunikacja między komponentami:** - **Porty analizy:** Przekazują dane z domeny operacyjnej do domeny analizy. - **Kolejki FIFO:** Używane do łączenia portów analizy z komponentami analizy, gwarantują, że nadawca nie blokuje kolejki. **Kodowanie komponentów OVM:** - **Część obiektowa (klasy):** Transakcja, agent, monitor, sterownik, generator sekwencji, tablica wyników. - **Część strukturalna (moduły):** Interfejs, DUT, moduł nadrzędny. - **Konfiguracja komponentów:** `set_config_int`, `get_config_int` itp. do zapisu/odczytu parametrów z bazy danych. ### UVM (Universal Verification Methodology) **Definicja:** Ewolucja OVM (pierwsze wydanie 2010), oparta na bibliotekach OVM 2.1.1. **Korzyści:** - Obsługuje modułowe i warstwowe komponenty weryfikacyjne SystemVerilog. - Umożliwia wielokrotne użycie komponentów, jasno definiuje funkcjonalność, pozwala na konfigurację. - Wydawany i utrzymywany przez Accellera, kod źródłowy dostępny. - Oparty na TLM, darmowy i open source. **Kluczowe komponenty testowe:** te same co w OVM (Generator, Sterownik, Agent, Monitor, Tablica wyników, Sequencer, DUT, Interfejs). **Główne różnice względem OVM:** - **Nazewnictwo:** Klasy `ovm_` zmienione na `uvm_`. - **Fazy UVM:** Zdarzeniowe fazy pracy testbencha, które automatyzują proces weryfikacji. - **Fazy build:** `build_phase`, `connect_phase`, `end_of_elaboration_phase`. - **Fazy symulacji:** `start_of_simulation_phase`, `run_phase` (z podfazami: `pre_reset`, `reset`, `post_reset`, `pre_configure`, `configure`, `post_configure`, `pre_main`, `main`, `post_main`, `pre_shutdown`, `shutdown`, `post_shutdown`), `extract_phase`, `check_phase`, `report_phase`, `final_phase`. - **Mechanizm konfiguracji:** Zamiast `set_config_object` i `get_config_object` używa klasy `uvm_config_db` z metodami `get`, `set`, `exists`, `wait_modified`. - **Kończenie testu:** Zamiast `global_stop_request()` używa mechanizmu `objection` (`raise_objection()`, `drop_objection()`). - **Warstwa rejestrów (`uvm_reg`):** Nowy typ klas do upraszczania operacji odczytu/zapisu do rejestrów i pamięci w DUT. - Metody dostępu do rejestrów: `write()`, `read()`, `mirror()`, `predict()`, `randomize()`, `update()`, `get()`.