Mnożenie liczb szesnastobitowych
![[implementacja mnożenia liczb szesnastobitowych]](code1.png)
Operacje modulo liczba całkowita
Przy weryfikacji systemów używających operacji arytmetycznych można
czasem zastosować abstrakcję danych wykorzystując przystawanie modulo pewne
ustalone m: h(i) = i mod m
Jak wiemy dla dodawania, odejmowania i mnożenia liczb całkowitych wynik
operacji modulo m zależy od wartości argumentów modulo m:
- ((i mod m)+(j mod m)) mod m = i+j (mod m)
- ((i mod m)-(j mod m)) mod m = i-j (mod m)
- ((i mod m)(j mod m)) mod m = ij (mod m)
Opis przystawania w BDD
- i = n mod m gdzie i jest zmienną całkowitą (rodziną k+1 zmiennych
bitowych), n i m są ustalone.
- Jeśli najbardziej znaczący bit i ma wartość 0, pozostałe muszą
reprezentować liczbę przystającą do n modulo m.
- Jeśli najbardziej znaczący bit i ma wartość 1, pozostałe muszą
reprezentować liczbę przystającą do n-2k modulo m.
- Jest tylko m wartości potencjalnie do rozważenia na każdym poziomie
więc rozmiar BDD jest O(mk)
Chińskie twierdzenie o resztach
Niech m1, m2, ..., mn będą względnie
pierwszymi liczbami naturalnymi,
m = m1 m2 ... mn.
Niech b, i1, i2, ..., in będą
liczbami
całkowitymi. Istnieje dokładnie jedno b <= i <= b+m, takie że
i = ij mod m dla 1 <= j <= n.
Jeśli więc zmienna całkowita x ma zawsze wartość mniejszą od m
jest jednoznacznie wyznaczona przez przystawanie do pewnych ij
modulo mj.
Weryfikacja
- AG (waiting & req & (in1 mod m = i) & (in2 mod m = j)
-> A(!ack U ack & (overflow | (output mod m = ij mod m))))
- i, j przebiegają od 0 do m-1
- m = 5, 7, 9, 11, 32
- Uwaga: zawsze zgłaszając przepełnienie spełniamy specyfikację
- BDD reprezentujące mnożenie rosną wykładniczo z czynnikami, zysk jest
więc duży mimo konieczności sprawdzenia m2 formuł.
Logarytmy
Chcemy dokładniej sprawdzić możliwość wystąpienia przepełnienia.
Reprezentujemy wartości zmiennych przez ich logarytmy.
- Niech h(i) = ceil(log(i+1))
- h(i)+h(j) <= 16, to h(ij) <= 16
- h(i)+h(j) >= 18, to h(ij) >= 17
- dla h(i)+h(j) = 17 przepełnienie może, ale nie musi wystąpić
Weryfikacja
- AG(waiting & req & (h(in1) + h(in2) <= 16) ->
A(!ack U ack & !overflow))
- AG(waiting & req & (h(in1) + h(in2) >= 18) ->
A(!ack U ack & overflow))
Weryfikacja układu przetwarzania potokowego
![[Schemat blokowy układu]](ALU.png)
Układ wykonujący operacje arytmetyczne i logiczne na danych
zawartych w zbiorze rejestrów. Można rozważać układy o różnym
rozmiarze rejestrów, różnej liczbie rejestrów w zbiorze
i różnej liczbie rejestrów potokowych.
Od liczby rejestrów potokowych zależy między innymi czas
przetwarzania pojedynczej instrukcji.
Rozważany tu model jest uproszczeniem, w rzeczywistym układzie
na zawartości rejestrów potokowych byłyby wykonywane dodatkowe operacje.
Największy zweryfikowany układ
- 64 rejestry w zbiorze rejestrów,
- 64 bity w każdym rejestrze,
- razem ponad 4096 bitów stanu,
- w efekcie ponad 101300 osiągalnych stanów
Abstrakcja
- Abstrakcja adresów rejestrów: stałe symboliczne ra, rb, rc
lub żaden z powyższych,
- Abstrakcja zawartości rejestrów: stałe symboliczne, ca, cb,
ca+cb, lub żadna z powyższych,
- Weryfikowana własność postaci
AG((srcaddr1=ra) & (srcaddr2=rb) & (dstaddr=rc) & !stall
-> AX AX((regra=ca) & (regrb=cb) -> AX(regrc=ca+cb)))
- AX związane z opóźnieniami w potoku
- Czas weryfikacji zależny liniowo od liczby i rozmiarów rejestrów,
- Największy układ zweryfikowany poprzednio miał 8 rejestrów
trzydziestodwubitowych, weryfikacja zajmowała podobny czas.
Jednak czas weryfikacji zależał kwadratowo od rozmiaru rejestru
i sześciennie od liczby rejestrów
Źródła