Metody weryfikacji użyte przy tworzeniu procesora Intel® Pentium® 4

Historia powstania procesora

• 1996 - Początek prac nad projektowaniem na strukturalnym na poziomie transferu rejestrów (SRTL).
  Początek prac nad weryfikacją modelu.
• 1997 - Powstanie pierwszego pełnego modelu SRTL.
• 1998 - Zakończenie projektowania na poziomie SRTL.
• Koniec 1999 - Wysłanie projektu do produkcji.
  Zakończenie teoretycznej fazy weryfkacji.
• Początek 2000 - Wyprodukowanie pierwszych egzemplarzy testowych.
  Rozpoczęcie weryfikacji krzemowego prototypu.
• Październik 2000 - Zatwierdzenie do masowej produkcji.
• Listopad 2000 - Pojawienie się na runku Pentium 4 taktowanych zegarem 1.4GHz i 1.5GHz.

Budowa procesora Pentium 4

Procesor Pentium 4 składa się z 42 milionów tranzystorów wykonanych w technologii 0.18u i połączonych sześcioma warstwami aluminiowych ścierzek. Kostka ma rozmiar 217 mm² i pobiera 55 watów (w wersji 1.5 GHz). Procesor ma przepustowość szyny 3.2 GB/sekundę. W Pentium 4 dodano 144 nowych 128-bitowych rozkazów SIMD (Single Instruction Multiple Data), które nazwano SSE2 (Streaming SIMD Extension 2).

Diagram 1: Uproszczony diagram blokowy Pentium 4

Diagram 2: Architektura Pentium 4

Potrzeba weryfikacji

Po tym jak błąd w procesorze Intel Pentium kosztował około 500 mln $, Intel zdał sobie sprawę z tego, że należy lepiej weryfikować modele procesorów jeszcze zanim trafią one do produkcji.

Specjalnie na potrzeby weryfikacji Pentium 4, został skompletowany zespól około 70 specjalistów. Rdzeń zespołu stanowiło 10 pracowników biorących poprzednio udział w weryfikacji procesora Pentium Pro. Dodatkowych 40 pracowników zatrudniono w 1997 roku wśród absolwentów college'ów. Kolejnych 20 pracowników zatrudniono w 1998 roku. Na wczesnym etapie prac, dużym wysiłkiem było wyszkolenie nowego personelu.

Oczywiście obecnie nie jest możliwa pełna formalna weryfikacja tak skomplikowanego urządzenia jak procesor Pentium 4. W związku z tym formalną weryfikację zastosowano tylko do niektórych fragmentów procesora takich jak jednostka zmiennoprzecinkowa czy układ dekodujący instrukcje.

Metody i narzędzia weryfikacji

Weryfikację Pentium 4 można podzielić na dwa etapy: najpierw przeprowadzono weryfikację modelu, a następnie weryfikację krzemowego prototypu. W każdym etapie zastosowano wiele metod i narzędzi.

Weryfikacja modelu

• Na potrzeby symulacji i weryfikacji zbudowano pełny model SRTL który działał w środowisku CSIM opracowanym w Intel Design Technology. Pełna symulacja działała z prędkością około 3-5Hz na komputerach Pentium 3 z systemem operacyjnym Linux.
  Łącznie wykonano około 2.384*10¹¹ cykli symulacji, co odpowiada około dwóm minutom pracy prawdziwego Pentium 4 1GHz.
• Na potrzeby symulacji i weryfikacji zbudowano 6 modeli CTE (Cluster Test Enviroment), z których każdy odpowiadał za inną część procesora i pozwalał na symulację tej części niezależnie od innych.
• Na początku, podczas tworzenia pełnego modelu procesora zastosowano metodologię "przodowania funkcjonalności" (feature pioneering). Polegała ona na tym, że kiedy nowa funkcjonalność była po raz pierwszy wprowadzana do modelu, weryfikator uruchamiał na niej swoje testy i w przypadku wykrycia błędu, opracowywał pierwszą wersję "łaty" razem z projektantem. Zwiększono w ten sposób szybkość integracji funkcjonalności oraz, przy okazji, przeszkolono weryfikatorów w pracy nad debugowaniem modelu.
• Do pomiaru pokrycia testami przestrzeni stanów używano narzędzia Proto z Intel Design Technology.
  Do momentu stworzenia prototypowego egzemplarza zebrano około 2.5mln warnunków na poziomie podukładów procesora i około 250 tys warunków pomiędzy podukładami. Za pomocą Proto zmierzono, że trafiono na około 90% warunków na poziomie podukładów i około 75% warunków pomiędzy układami.
• W celu zmierzenia liczby wykorzystywanych ścieżek w mikrokodzie użyto narzędzia Pathfinder z Intel's Central Validation Group. Okazało się, że w zwykłych przypadkach wykorzystywane jest <10% mikrokodu. Pozostała część dotyczyła sytuacji wyjątkowych (np. błąd pamięci) wiec okazało się, że należy te przypadki dopisać do testów, żeby uzyskać większe pokrycie.
• Model Checking zastosowano przy użyciu narzędzia Prover opracowanego w Intel Design Technology. Model wyspecyfikowano w FSL (Formal Specification Language).
  Model Checking'u użyto między innymi do weryfikacji protokołu szyny.
• Do weryfikacji jednostki zmiennoprzecinkowej użyto mieszanki STE (Symbolic Trajectory Evaluation) oraz dowodzenia twierdzeń.
• Do weryfikacją metodą dowodzenia twierdzeń w Intel używa się narzędzia HOL Light opartego na logice wyższego rzędu. HOL Light zaimplementowano w CAML Light oraz Objective CAML.
• Do momentu wytworzenia prototypowego egzemplarza łącznie zebrano około 10000 dowodów na których weryfikowano model.
• W związku z tym, że każdy fragment procesora z założenia powinien był być energo-oszczędny, musiał on zwalniać przy małym obciążeniu ignorując niektóre cykle zegara (tzw. clock gating).
  W celu sprawdzenia, czy nie wystąpią z tego powodu jakieś dodatkowe błędy (np. gdy jeden z podukładów "zaśnie", a drugi będzie od niego czegoś oczekiwać i się nie doczeka) były opracowane dodatkowe warunki, które były sprawdzane oraz opracowano metodę testowania modelu (temporal divergence testing) polegającą na przeprowadzeniu tego samego testu z włączonym oszczędzaniem energii oraz bez niego i porównaniu wyników.
• Po każdej zmianie modelu przeprowadzano testy regresyjne.

Weryfikacja krzemowego prototypu

• Ważną częścią weryfikacji prototypowego procesora jest jego interakcja z układam zewnętrzymi (pamięć, szyna, chipset), więc jest to jedna z głównych testowanych grupy wlasności.
• Działającego układu nie da się już tak dobrze debugować jak modelu między innymi dlatego, że działa on z pełną prędkością. Należało więc przygotować odpowiednie środowiska do testowania własności systemu.
• Wykorzystano metodę testu losowych instrukcji (RIT) które były generowane przez specjalne generatory np. pod kątem testu architektury zbioru instrukcji (ISA).
• Przygotowano testy z losowymi danymi oraz losowymi danymi zmiennoprzecinkowymi dla jednostki zmiennoprzecinkowej.
• Osobno przygotowano testy specjalnych przypadków brzegowych.
• Na wszystkich przygotowanych testach porównywano działanie modelu do prototypowego procesora.

Wykryte błędy

Dwa z wykrytych za pomocą formalnej weryfikacji błędów, to przykłady klasycznych problemów z dziedziny obliczeń zmiennoprzecinkowych:

1. W instrukcji FADD dla pewnej kombinacji argumentów 72-bitowy sumator ustawiał bit przeniesienia na 1, gdy nie występowało przeniesienie.
   
2. W instrukcji FMUL bit "sticky" nie był poprawnie ustawiany dla pewnych kombinacji wartości mantys argumentów, przy ustawionym trybie zaokrąglania do góry. Konkretnie:
   src1[67:0] := X*2⁽ⁱ⁺¹⁵⁾ + 1*2ⁱ
   src2[67:0] := Y*2^(j+15) + 1*2^j
   gdzie i+j = 54 i {X,Y} są dowolnymi 68-bitowymi liczbami całkowitymi.
   Zauważmy, że błąd ten prawdopodobnie nigdy nie zostałby znaleziony w praktyce, gdyż szansa jego wystąpienia dla losowych liczb wynosi około 1 do 5*10²⁰ .

Omówienie znalezionych błędów

W procesorze Pentium 4 udało się wykryć 350% więcej błędów niż w procesorze Pentium Pro. Przy aktualnie zastosowanej metodologii, procent wykrytych błędów jest zbliżony do 100%.

Łączny rozkład błędów:

• Błędy w zapisie projektu RTL (Register Transfer Level) (18,1%) - literówki, błędy przy kopiowaniu, niepoprawne asercje w kodzie SRTL albo niezrozumienie specyfikacji.
• Mikroarchitektura (25,1%) - problemy z definicją mikroarchitekrury, niedostateczna komunikacja między architektami i projektantami systemu, błędna dokumentacja protokołów, algorytmów itd.
• Zmiany w logice i mikrokodzie (18,4%) - błędy powstałe w wyniku zmian w projekcie, niezainicjowany stan po resecie lub błędy związane z ograniczaniem dostępu do zegara.
• Architektura (2,8%) - pewne własności zosały dokładnie zdefiniowane dopiero w toku projektowania i były "upychane", aby jakoś działały.

Błędy znalezione podczas pracy w poszczególnych zespołach:

• Walidacja systemu (71%) - najlepsze środowisko do weryfikacji gotowego produktu. Przy jego pomocy znaleziono szeroki wachlarz błędów logicznych i układowych.
• Walidacja kompatybilności (7%) - mimo że nie znaleziono tak wielu błędów jak w walidacji systemowej, te które znaleziono pojawiają się w prawdziwych aplikacjach i systemach operacyjnych.
• Zespół narzędzi debugujących (6%) - większość błędów wykryto podczas pierwszych tygodni testów na prototypie A-0. Podkreśla to wagę zastosowania narzędzi debugujących w początkowych etapach testowania sprzętu.
• Walidacja chipsetu (5%) - Ten zespół skupia się na magistrali i operacjach wejścia/wyjścia i odzwierciedlają to znalezione przez nich błędy: dotyczą one głównie protokołów magistrali.
• Zespół architektury procesora (4%) - badają wydajność i prowadzą generalne testy systemu. Ta grupa odpowiada też za debugowanie błędów zgłoszonych przez inne zespoły.
• Zespoły projektowania platformy sprzętowej i inne (7%) - obejmuje grupy projektowania sprzętu, które rozwijają i wdrażają walidację, oraz zespół projektowania procesora, zaspół walidacji przed-sprzętowej (teoretycznej).

Źródła i dodatkowe materiały

• Validating The Intel® Pentium® 4 Processor
• The Microarchitecture of the Pentium® 4 Processor
• Validating The Intel® Pentium® 4 Microprocessor
• Intel’s Successes with Formal Methods
• The Intel Case Study & Harry Foster's Assertion Checkers Hell
• Verification and Testbenches