Weryfikacja funkcjonalna

Weryfikacja funkcjonalna polega na sprawdzeniu, czy projekt logiki jest zgodny ze specyfikacją. Weryfikacja funkcjonalna jest próbą odpowiedzi na pytanie „Czy proponowany projekt robi to, co zamierzono?” Jest to złożone i zajmuje większość czasu i wysiłku (do 70% czasu projektowania i rozwoju) w większości dużych projektów projektowania systemów elektronicznych. Weryfikacja funkcjonalna jest częścią szerszej weryfikacji projektu , która oprócz weryfikacji funkcjonalnej uwzględnia aspekty niefunkcjonalne, takie jak czas, układ i moc.

Tło

Chociaż liczba tranzystorów rosła wykładniczo zgodnie z prawem Moore'a , zwiększenie liczby inżynierów i czasu potrzebnego na wyprodukowanie projektów wzrasta tylko liniowo . W ten sposób do automatyzacji projektowania elektronicznego (EDA), aby sprostać złożoności projektowania tranzystorów. Języki takie jak Verilog i VHDL są wprowadzane wraz z narzędziami EDA. Większość błędów w kodowaniu logicznym wynika z nieostrożnego kodowania (12,7%), błędnej komunikacji (11,4%) i wyzwań związanych z mikroarchitekturą (9,3%).

Weryfikacja funkcjonalna jest bardzo trudna ze względu na ogromną liczbę możliwych przypadków testowych, które istnieją nawet w prostym projekcie. Często możliwych jest ponad 10^80 testów, aby kompleksowo zweryfikować projekt – liczba niemożliwa do osiągnięcia w ciągu całego życia. Ten wysiłek jest równoważny weryfikacji programu i jest NP-trudny lub nawet gorszy – i nie znaleziono rozwiązania, które działałoby dobrze we wszystkich przypadkach. Można go jednak zaatakować na wiele sposobów. Żadna z nich nie jest idealna, ale każda może być pomocna w pewnych okolicznościach:

  • Symulacja logiczna symuluje logikę przed jej zbudowaniem.
  • Przyspieszenie symulacji stosuje sprzęt specjalnego przeznaczenia do problemu symulacji logicznej.
  • Emulacja buduje wersję systemu za pomocą programowalnej logiki. Jest to drogie i wciąż znacznie wolniejsze niż prawdziwy sprzęt, ale o rząd wielkości szybsze niż symulacja. Można go użyć na przykład do uruchomienia systemu operacyjnego na procesorze.
  • Weryfikacja formalna próbuje udowodnić matematycznie, że pewne wymagania (również wyrażone formalnie) są spełnione lub że pewne niepożądane zachowania (takie jak zakleszczenie) nie mogą wystąpić.
  • Inteligentna weryfikacja wykorzystuje automatyzację, aby dostosować testbench do zmian w kodzie poziomu transferu rejestru .
  • lint specyficzne dla HDL i inne heurystyki są używane do znajdowania typowych problemów.

typy

Istnieją trzy rodzaje weryfikacji funkcjonalnej, a mianowicie: dynamiczna weryfikacja funkcjonalna, hybrydowa dynamiczna funkcjonalno-statyczna oraz weryfikacja statyczna.

Weryfikacja oparta na symulacji (zwana także „ weryfikacją dynamiczną ”) jest szeroko stosowana do „symulowania” projektu, ponieważ ta metoda bardzo łatwo skaluje się. Bodziec jest dostarczany do ćwiczenia każdej linii w kodzie HDL. Stanowisko testowe jest zbudowane w celu funkcjonalnej weryfikacji projektu poprzez dostarczanie znaczących scenariuszy w celu sprawdzenia, czy przy określonych danych wejściowych projekt działa zgodnie ze specyfikacją.

Środowisko symulacyjne zazwyczaj składa się z kilku rodzajów komponentów:

  • Generator generuje wektory wejściowe, które służą do wyszukiwania anomalii występujących między intencją (specyfikacją) a implementacją (kod HDL) . Ten typ generatora wykorzystuje NP-zupełny typ Solvera SAT, który może być kosztowny obliczeniowo. Inne typy generatorów obejmują ręcznie tworzone wektory, zastrzeżone generatory generatorów opartych na wykresach (GBM). Nowoczesne generatory tworzą ukierunkowane losowe i losowe bodźce, które są statystycznie napędzane w celu weryfikacji losowych części projektu. Losowość jest ważna, aby osiągnąć wysoką dystrybucję w ogromnej przestrzeni dostępnych bodźców wejściowych. W tym celu użytkownicy tych generatorów celowo zaniżają wymagania dotyczące generowanych testów. Zadaniem generatora jest losowe wypełnienie tej luki. Ten mechanizm pozwala generatorowi tworzyć dane wejściowe, które ujawniają błędy, których nie szuka bezpośrednio użytkownik. Generatory również przekierowują bodźce w kierunku projektowania przypadków narożnych, aby jeszcze bardziej podkreślić logikę. Odchylenie i losowość służą różnym celom i istnieją między nimi kompromisy, stąd różne generatory mają inną mieszankę tych cech. Ponieważ dane wejściowe do projektu muszą być prawidłowe (legalne) i należy zachować wiele celów (takich jak odchylenia), wielu generatorów stosuje problemu spełnienia ograniczeń (CSP) do rozwiązywania złożonych wymagań testowych. Modelowana jest legalność danych wejściowych projektu i arsenał odchyleń. Generatory oparte na modelach wykorzystują ten model do wytwarzania odpowiednich bodźców dla projektu docelowego.
  • Sterowniki przetwarzają bodźce wytwarzane przez generator na rzeczywiste dane wejściowe dla weryfikowanego projektu . Generatory tworzą dane wejściowe na wysokim poziomie abstrakcji, a mianowicie jako transakcje lub język asemblera. Sterowniki przetwarzają te dane wejściowe na rzeczywiste dane wejściowe projektu, zgodnie z definicją w specyfikacji interfejsu projektu.
  • Symulator generuje dane wyjściowe projektu w oparciu o bieżący stan projektu (stan przerzutników) i wprowadzone dane wejściowe . Symulator posiada opis projektu net-list. Ten opis jest tworzony przez syntezę HDL do listy sieci niskiego poziomu bramki.
  • Monitor przekształca stan projektu i jego dane wyjściowe na poziom abstrakcji transakcji, dzięki czemu można go przechowywać w bazie danych „tablic wyników” do późniejszego sprawdzenia .
  • Kontroler sprawdza, czy zawartość „tablic wyników” jest zgodna z prawem. Istnieją przypadki, w których generator oprócz danych wejściowych generuje oczekiwane wyniki. W takich przypadkach kontroler musi sprawdzić, czy rzeczywiste wyniki odpowiadają oczekiwanym.
  • Kierownik ds. arbitrażu zarządza łącznie wszystkimi powyższymi składnikami.

różne wskaźniki pokrycia , aby ocenić, czy projekt został odpowiednio wykonany. Obejmują one pokrycie funkcjonalne (czy wykorzystano wszystkie funkcje projektu?), pokrycie instrukcji (czy wykorzystano każdą linię HDL?) oraz pokrycie gałęzi (czy wykorzystano każdy kierunek każdej gałęzi?).

Narzędzia

  • Aldec
  • Urządzenia strzałkowe
  • Avery Design Systems: SimCluster (do symulacji logiki równoległej) i Insight (do weryfikacji formalnej)
  • Breker Verification System: Trek (oparte na modelu narzędzie do generowania testów dla złożonych SoC)
  • Systemy projektowania kadencji
  • EWA/ZeBu
  • Grafika Mentora
  • Technologia Nusym
  • Oprogramowanie obsydianowe
  • Rozwiązania OneSpin
  • Prawdziwy zamiar: Statyczne podpisywanie
  • Streszczenie
  • Valtrix Systems: Sting (wszechstronne narzędzie do weryfikacji projektu dla złożonych implementacji SoC/CPU)

Zobacz też

Pobrano z „ https://en.wikipedia.org/w/index.php?title=Functional_verification&oldid=1141153889 ”