Jak sprawdzić, czy bitfile z Vivado pochodzi z danego kodu źródłowego?

Potrzebuję ustalić, czy bitfile z Vivado powstał z kompilacji określonego kodu źródłowego. Sam bitfile przy każdej kompilacji jest inny - wynika to ze stosowania losowej optymalizacji, być może tylko na etapie rozmieszczania elementów (placement przy implementacji) i tworzenia połączeń (routing w następnej fazie implementacji) - gdyby więc z bitfile odtworzyć schemat logiki, to dla każdej kompilacji powinien być taki sam.

Kompilacja od kodu źródłowego do bitfile składa się z trzech głównych etapów: syntezy (przetworzenie kodu źródłowego na schemat logiki, z dobraniem typów elementów), implementacji (w tym rozmieszczenia elementów - wyboru, które elementy FPGA mają stać się którymi elementami schematu logiki - ale nawet tam jeszcze typy elementów wybrane przy syntezie mogą być zamieniane na inne, o równoważnym działaniu; oraz utworzenia połączeń), i przetworzenia utworzonego układu elementów FPGA na bitfile.

Logika, jaką realizuje skompilowany program, powinna zależeć wyłącznie od kodu źródłowego - więc porównanie logiki po jej odtworzeniu z bitfile powinno rozpoznać, czy bitfile pochodzi z danego kodu źródłowego, czy nie. Tylko czy jest do tego odpowiedni program - zarówno do przetworzenia bitfile na logikę, jak i na porównanie logiki z bitfile z logiką z kodu źródłowego?

_jta_ napisał:

wynika to ze stosowania losowej optymalizacji

Pewien jesteś tego stwierdzenia ?
Szło by poprzek dobrym praktykom inżynierskim, tak jakby nowe rysunki np mostu ze względu na oświetlenie były inne.

Obracam się z nieco innych kręgach, i losowe (ale za to bardo silne) występuje w szyfrowaniu, czasem w sieciach jako lekarstwo na kolizje
Z interpretacją "losową" trudno sobie wyobrazić większość scenariuszy produkcyjnych inżynierii "na komputerach" - ale zaznaczam, Bozia ma różnych lokatorów

Spotkałem tylko raz opcję "deterministic" defaultowo true - w Microsoft Visual Studio
Tam false sie daje jeśli z każdym buildem numer wersji ma automatycznie kroczyć. Ale to dotyczy tylko jednego / dwóch pól a reszta binarki jest taka sama.

_jta_ napisał:

Logika, jaką realizuje skompilowany program, powinna zależeć wyłącznie od kodu źródłowego

Oczywiście tak, dlatego zdziwienie

JacekCz napisał:

Pewien jesteś tego stwierdzenia ?

Tak, znalazłem tę informację w jednym z opisów Vivado. I widzę, że każda kompilacja z tych samych źródeł daje inny wynik.

Niestety wynik syntezy zrobionej z tych samych źródeł też jest za każdym razem inny - losowość nie ogranicza się do implementacji:

JacekCz napisał:

Spotkałem tylko raz opcję "deterministic" defaultowo true - w Microsoft Visual Studio
Tam false sie daje jeśli z każdym buildem numer wersji ma automatycznie kroczyć. Ale to dotyczy tylko jednego / dwóch pól a reszta binarki jest taka sama.

Temat deterministycznej kompilacji stał się popularny w ubiegłej dekadzie, jako metoda zwiększenia zaufania do softu. Nie jest to oczywiste i wymaga sporo pracy od twórców narzędzi.
Dla przykładu C# https://blog.paranoidcoding.org/2016/04/05/deterministic-builds-in-roslyn.html - to jest blog Jareda Parsona, jednego z programistów kompilatora C#.

W temacie wątku. Kilkakrotnie przeszukiwałem sieć w czasie ostatnich 20 lat. Znajdowałem jedynie bardzo niskopoziomowe efekty inżynierii odwrotnej bitfile dla konkretnych typów FPGA plus dużo opisów jakie to bardzo trudne. Nigdy nie widziałem śladu narzędzi do odtworzenia logiki z bitfile.

Podejrzewam, że istnieją, ale nie są ani łatwo dostępne, ani legalne - i są używane przez speców od kopiowania algorytmów (taki spec dostaje bitfile, a robi z tego program w postaci źródłowej) - kiedyś mi opowiadano, jak kopiowano układy scalone (i to takie złożone): szlifowano po kawałku, fotografowano pod mikroskopem, i na koniec według tych zdjęć robiono maski do produkcji kopii - to było w czasach komunistycznych i służyło do zrobienia własnej produkcji tego, czego nie chciano nam sprzedawać.