Intel Keynote On Formal A Mind-Stretcher

Opublikowane ponownie przez Plato

Obserwuje: 0

Firma Synopsys zamieściła w witrynie SolvNet fascynujące przemówienie wygłoszone przez dr Theo Drane'a z Intel Graphics. Tematem jest sprawdzanie równoważności ścieżki danych. Może to brzmieć jak kolejne formalne poparcie DPV Synopsys VC, ale i tak powinieneś to obejrzeć. Jest to poszerzająca umysł dyskusja na temat zastosowań i rozważań formalnych, która wyprowadzi Cię poza rutynowy przewodnik użytkownika na bardziej fascynujące terytorium.

Prezentacja Intela dotycząca formalności

Intelektualne zrozumienie a testowanie próbek

Symulacja oparta na testach we wszystkich jej postaciach jest doskonała i często niezastąpiona przy weryfikacji poprawności specyfikacji projektu lub wdrożenia. Rozpoczęcie jest również łatwe. Wystarczy napisać program testowy i rozpocząć symulację. Ale drugą stroną tej prostoty jest to, że nie musimy tego robić w pełni aby zacząć, zrozum, co testujemy. Przekonujemy samych siebie, że dokładnie przeczytaliśmy specyfikację i rozumiemy wszystkie przypadki narożne, ale nie potrzeba dużej złożonej złożoności, aby przytłoczyć nasze zrozumienie.

Formalny zachęca do głębokiego zrozumienia funkcjonalności (przynajmniej jeśli chcesz dostarczyć wartościowy wynik). W powyższym przykładzie proste pytanie – czy z może mieć zawsze same jedynki – nie demonstruje przykładu w ciągu miliarda cykli na symulatorze. Nic dziwnego, ponieważ jest to ekstremalny przypadek narożny. Formalny test dostarcza konkretnego i bardzo nieoczywistego przykładu w 1 sekund i może wykazać, że jest to jedyny taki przypadek w nieco krótszym czasie.

OK, formalnie zrobił to, czego nie potrafiły testy dynamiczne, ale co ważniejsze, nauczyłeś się czegoś, czego symulator mógł ci nigdy nie powiedzieć. Że istnieje tylko jeden możliwy przypadek, w którym taki stan może zaistnieć. Formalny pomógł ci lepiej zrozumieć projekt na poziomie intelektualnym, a nie tylko jako probabilistyczne podsumowanie w skończonym zestawie przypadków testowych.

Problemy ze specyfikacją

Następny przykład Theo opiera się na automacie z błędami (tzw. automacie, ponieważ po naciśnięciu przycisku pojawia się błąd). Wygląda to na całkiem prosty problem sprawdzania równoważności C do RTL, model C po lewej stronie, model RTL po prawej. Jedną z niespodzianek dla Theo na początku jego formalnej kariery było to, że zachowanie przesunięcia w prawo w modelu C nie jest całkowicie zdefiniowane w standardzie C, mimo że gcc będzie zachowywać się rozsądnie. Jednakże DPV będzie narzekać na niedopasowanie w porównaniu z RTL, tak jak powinno. Niezdefiniowane zachowanie jest niebezpieczną rzeczą, na której można polegać.

Formalny jak automat z owadami

Porównanie specyfikacji C i RTL wiąże się z innymi zagrożeniami, szczególnie w przypadku szerokości bitów. Obcięcie lub utrata bitu przenoszenia w sygnale pośrednim (#3 powyżej) są dobrymi przykładami. Czy są to problemy ze specyfikacją? Może szara strefa między wyborem specyfikacji a implementacją.

Poza sprawdzaniem równoważności

Wydaje się, że głównym celem DPV jest sprawdzenie równoważności między referencją C lub RTL a implementacją RTL. Jednak taka potrzeba występuje stosunkowo rzadko i istnieją inne przydatne sposoby zastosowania takiej technologii, jeśli są trochę gotowe do użycia. Najpierw klasyk w świecie wdrożeń – wprowadziłem zmianę, naprawiłem błąd – czy w rezultacie wprowadziłem jakieś nowe błędy? Trochę jak sprawdzanie SEQ po dodaniu bramkowania zegara. W niektórych przypadkach analiza osiągalności w wynikach bloków może być kolejnym przydatnym zastosowaniem.

Nie tylko sprawdzanie równoważności

Theo staje się jeszcze bardziej kreatywny, prosząc uczestników szkolenia o wykorzystanie przykładów przeciwnych, aby lepiej zrozumieć projekt, rozwiązać Sudoku or rozkładać na czynniki liczby całkowite. Przyznaje, że DPV jest dziwnym sposobem podejścia do takich problemów, ale wskazuje, że jego zamiarem jest przełamanie iluzji, że DPV służy wyłącznie do sprawdzania równoważności. Ciekawy pomysł i z pewnością wyczerpujące myślenie o takich wyzwaniach. (Przyznaję, że natychmiast zacząłem myśleć o problemie Sudoku, gdy tylko o nim wspomniał.)

Zakończyć

Theo kończy dyskusją na temat metodologii ważnych w zastosowaniu produkcyjnym, wokół ograniczeń, regresji i porównań ze starszymi modelami RTL. Również wyzwania związane z ustaleniem, czy to, co sprawdzasz, rzeczywiście odpowiada specyfikacji języka naturalnego najwyższego poziomu.

Bardzo energetyzujące wystąpienie, warte obejrzenia tutaj, w SolvNet!

Udostępnij ten post przez: