\chapter{Formal Synthesis}
Spesifikasi diimplementasikan melalui proses sintesa ({\em synthesis}).
Proses sintesa dapat dilakukan secara manual atau secara otomatis.
Pembuatan implementasi secara manual hanya cocok untuk desain yang
tingkat kompleksitasnya tidak terlalu tinggi.
Untuk sistem yang kompleks, kesalahan sangat mudah terjadi
({\em error prone}).

Proses sintesa yang otomatis disebut ``automatic synthesis''.
Untuk menjamin kebenaran proses sintesa, maka setiap langkah dari
proses sintesa tersebut harus dibuktikan kebenarannya.
Proses sintesa ini dilakukan secara bertahap dimana setiap
tahap dilakukan pembuktian ({\em proof}) sehingga hasil sintesa
akan benar karena {\em correct by construction}.

{\em Formal synthesis} ini biasanya berangkat dari spesifikasi yang
dibuat secara formal, kemudian dilakukan proses {\em refining}
sehingga diperoleh hasil yang lebih detail - menuju ke level
abstraki yang lebih rendah (implementasi).
Proses ini dilakukan berulang-ulang sampai akhirnya menjadi implementasi
yang diinginkan. Dalam desain VLSI, proses ini dilakukan sampai
menjadi level layout dari transistor.
Setiap langkah pada proses {\em refining} ``dijaga'' oleh sebuah
mekanisme, misalnya dengan menggunakan sebuah {\em theorem prover}
sehingga tidak dapat melakukan proses {\em refining} yang salah.