ABV - Assertions Based Verification
Asercje to temat ściśle związany z poprzednio omawianym tematem Constrained Random Verification. Stosując nowoczesne języki do weryfikacji możemy wygenerować bardzo duży zestaw wymuszeń dla testowanego układu. Często zdarza się, że czas symulacji projektu razem z pełnym testbench'em zajmuje kilka dni. Powstaje zatem problem z uruchamianiem i odpluskwianiem (ang. debugging) takiego projektu. Czas potrzebny na propagacje błędu od jego źródła do wyjść testowanego układu może być bardzo długi. Często błędy w działaniu układu ujawniają się na wyjściach wiele godzin później podczas symulacji. Projektant może spędzić kilka dni uruchamiając kolejne symulacje i szukając źródła błędu. Można również uruchomić jedną symulacje z rejestracją wszystkich możliwych sygnałów w projekcie na potrzeby debugging'u. Ale i to wymaga sporo czasu ponieważ pełna rejestracja stanu symulowanego układu znacząco spowalnia proces symulacji.
Z pomocą przychodzą tutaj asercje. Czyli dedykowany kod, który kontroluje działanie układu i raportuje natychmiastowo wykryte błędy. Asercje były stosowane od dawna w językach opisu sprzętu. W języku VHDL mamy konstrukcje assert. W języku Verilog-HDL asercje były opisywane przy użyciu konstrukcji if(...) $display. Aczkolwiek weryfikacja z użyciem asercji została w ostatnich latach znacząco uporządkowana i sformalizowana.
Umieszczanie asercji w projekcie przynosi następujące zyski:
-
Wykrywanie błędów u źródła. Czyli znaczne skrócenie procesu odpluskwiana.
-
Dokumentacja działania układu w postaci wykonywalnego kodu.
-
Analiza jakości testbench'a poprzez wykrywanie poprawnych operacji wykonanych przez układ.
Należy tutaj dodać, że asercje nie są tylko wykorzystane do wykrycia błędów. Możemy przy pomocy asercji również wykrywać poprawne operacje aby sprawdzić czy nasz układ jest wyczerpująco testowany.
Ze względu na rosnącą popularność asercji wiele firm rozpoczęło prace nad narzędziami do weryfikacji formalnej. Narzędzia takie potrafią poprzez statyczną analizę kodu wykryć te asercje, które zgłoszą błędy również podczas symulacji. Statyczna analiza jest znacznie szybsza od symulacji i ewentualne informacje o błędach otrzymujemy praktycznie natychmiastowo. Jest to jednak trudne zagadnienie i wymaga od użytkownika definiowania zakresu możliwych stanów wejść układu. W związku z tym symulacja czyli dynamiczny sposób sprawdzania asercji jest obecnie najczęściej używany.
Asercje mają opisywać zamierzenie projektanta odnośnie funkcjonalności danego modułu czy interfejsu. Opracowano kilka języków do opisu asercji ale mają one podobną strukturę. Składnia dopuszcza definiowanie równań boolowskich oraz tworzenie sekwencji tych równań odpowiednio rozmieszczonych w czasie. Przykładem takiego języka jest PSL (Property Specification Language) . Poniżej przykład w języku VHDL razem z asercjami zapisanymi przy pomocy języka PSL:
process(CLK, RESET)
begin
if(rising_edge(CLK)) then
if(RESET='1') then
shift_reg <= (others=>'0');
else
if(CLK_EN='1') then
shift_reg <= shift_reg(SIZE-2 downto 0) & SHIFT_IN;
end if;
end if;
end if;
end process;
SHIFT_OUT <= shift_reg(SIZE-1);
--psl ChReset: assert always (RESET -> next(or_reduce(shift_reg)='0')) @rising_edge(CLK);
--psl ChShift: assert always ({CLK_EN[*SIZE]} |-> {SHIFT_OUT=prev(SHIFT_IN, SIZE)}) abort RESET @rising_edge(CLK);
--psl CrShift: cover({not RESET and CLK_EN; shift_reg(0)=prev(SHIFT_IN)}) @rising_edge(CLK);
Pisząc w języku HDL projektant skupia się nad pojedynczymi cyklami działania układu. Podczas gdy używają języka do opisu asercji skupiamy się na sekwencji zdarzeń jakie mają wystąpić w układzie. Zatem jest mało prawdopodobne, że w obu przypadkach popełnimy te same błędy. W języku PSL podzielony jest na cztery warstwy:
-
Warstwa równań boolowskich. Tutaj określamy równania boolowskie, które identyfikują zdarzenia jakie mają wystąpić w naszym projekcie.
-
Warstwa czasowa. Gdzie możemy określić rozłożenie w czasie poszczególnych zdarzeń czyli utworzyć sekwencje.
-
Warstwa weryfikacji. Ta warstwa definiuje w jaki sposób należy traktować daną sekwencje. Sekwencja może definiować poprawne działanie układu i ewentualne odstępstwa powinny być zgłaszane jako błąd. Ale również taka sekwencja może identyfikować pewne zdarzenia, które określają wykonanie testu na danym fragmencie projektu.
-
Warstwa modelowania. Tutaj pojawiają się dodatkowe konstrukcje czy fragmenty kodu, które są niezbędne do zdefiniowania asercji. Warstwa ta jest wykorzystywana głównie do weryfikacji formalnej.
Zaletą języka PSL jest wiele wariantów jego składni. Jeżeli używamy tego języka w projekcie VHDL, wówczas do modelowania asercji używamy operatorów i funkcji języka VHDL. Podobnie jest w języku Verilog-HDL czy SystemC. PSL korzysta z operatorów i funkcji które już są dostępne w tych językach i nie definiuje takich samych operatorów we własnej składni.
Asercje bardzo dobrze sprawdzają się w wykrywaniu następujących błędów:
-
Niepoprawne wymuszenia
-
Niepoprawne połączenia w projekcie
-
Operacje niezgodne z protokołem danego interfejsu
-
Propagacja wartości X,U w układzie
-
Błędy funkcjonalne poszczególnych modułów
Stosowanie asercji nawet w prostych projektach znacznie upraszcza prace i podnosi jakość weryfikacji. Czas poświęcony na pisanie asercji zwraca się zwłaszcza gdy po pewnym czasie wracamy do naszego projektu i integrujemy go z innymi modułami tworząc większy system. Asercje znacząco upraszczają prace integracyjne i późniejszą weryfikacje systemu.
|
Strona Główna
