\chapter{Formal Verification}

\begin{quote}
{\em Non-exhaustive testing can be used to show the presence of bugs,
but never to show their absence. (E. W. Dijkstra)}
\end{quote}

\begin{quote}
{\em The real benefit of verification schemes is not in proving anything
absolutely but in pinpointing defects along its way.\\
(Ivar Peterson in ``Fatal Defect'' quoting Peter Neumann)}
\end{quote}

Tujuan dari formal verification adalah membuktikan bahwa sebuah implementasi
betul-betul mengimplementasikan apa-apa yang dijabarkan dalam spesifikasinya.
Formal verification dapat juga digunakan untuk menjabarkan kebenaran
dalam proses translasi.
Ketika kita melakukan proses translasi - misalnya dalam proses optimasi -
bagaimana kita menjamin bahwa rangkaian yang dihasilkan masih memiliki
fungsi yang sama (ekivalen) dengan rangkaian sebelumnya.

Formal verification dapat dilakukan dengan menggunakan:
\begin{itemize}
\item equivalence checker
\item model checker
\item therem prover
\end{itemize}



\section{Equivalence Checking}
{\em Equivalence checking} dengan menggunakan {\em equivalence checker}
membandingkan dua buah rangkaian dan membuktikan bahwa keduanya memiliki
fungsi yang ekivalen.
Proses yang dilakukan mencoba menjawab pertanyaan: ``Apakah perubahan
yang telah saya lakukan terhadap desain ini mengubah fungsinya?''
Pertanyaan ini dapat terjadi ketika kita melakukan proses optimasi terhadap
rangkaian. Misalnya, kita ingin agar rangkaian lebih hemat dalam menggunakan
catu daya dengan mengorbankan {\em performance}, maka kita ubah rangkaiannya
dengan mengurangi beberapa komponen.

Proses {\em equivalence checking} ini dapat dilakukan dengan berbagai cara,
mulai dari manual sampai ke otomatisasi dengan menggunakan {\em Ordered
Binary Decision Diagram} (OBDDs).


\section{Model Checking}
Model checking menangani masalah yang berbeda dengan equivalence checking.
Dalam model checking, kita ingin menguji apakah desain ini memiliki
sifat ({\em properties}) seperti yang kita harapkan?
Singkatnya kita ingin membuat sebuah model abstrak dari desain kita,
kemudian kita mencoba membuktikan properties dari desain tersebut misalnya
apakah akan terjadi {\em deadlock} atau {\em livelock}.

Sudah ada beberapa tools untuk melakukan model checking, akan tetapi
kebanyakan masih berupa tools yang dikembangan untuk model berukuran
kecil sebagai riset di perguruan tinggi.



\section{Theorem Proving}
Metoda yang menggunakan pendekatan {\em theorem proving} dapat dikatakan
duduk di atas kedua metoda yang telah dibahas sebelumnya.
Theorem proving dengan menggunakan theorem prover memiliki {\em features}
yang lebih komplit. Sayangnya teknologi theorem proving ini masih
baru dan tools yang ada masih sulit untuk digunakan.

Theorem prover merupakan tools yang dapat membantu desainer untuk
membuktikan {\em property} dari sebuah sistem. Dia menjaga agar pengguna
tools tersebut tidak melakukan langkah-langkah yang salah, seperti
misalnya mengganti sebuah komponen dengan komponen yang berbeda fungsinya.
Theorem prover masih membutuhkan bantuan pengguna untuk mengarahkan
atau mengambil langkah-langkahnya.


\section{Binary Decision Diagram (BDD)}


\section{Verification Tools}
Adanya tools mendekatkan metoda formal kepada realitas sehingga betul-betul
dapat dimanfaatkan dalam desain sesungguhnya, bukan desain dalam ukuran
mainan saja.
Dalam beberapa bagian telah disinggung beberap tools. Berikut ini daftar
beberapa tools yang telah tersedia.

\begin{itemize}
\item SPIN: PROMELA tools
\item Formality
\item HOL Theorem Prover
\item BDD tools
\item Larch Prover
\end{itemize}