Abstrak Nama : Dwi Teguh Priyantini Program Studi : Magister Ilmu Komputer Judul : Formalisasi Algoritma Aritmatika dan Konstruksi Terkait pada VHDL dengan HOL Theorem Prover Padapengembangansistem,dibutuhkansebuahmekanismeuntukmenjaminbahwa sistem tersebut berjalan dengan benar tanpa error atau ’bug’. Sejauh ini, hal yang biasadilakukanadalahdengantesting,tetapihalinisulitdilakukanuntukmencakup semua kemungkinan. Untuk sistem yang membutuhkan tingkat correctness yang tinggi, seperti misalnya pada hardware , perlu mekanisme yang dapat menjamin kebenaran program untuk semua kemungkinan input. Ada solusi lain yang dapat menjamin kebenaran program untuk semua kemungkinan input, yaitu dengan verifikasi formal. Verifikasi formal dilakukan dengan pemodelan matematika. Salah satu sistem yang membutuhkan tingkat correctness yang tinggi adalah sistem bilangan floating-point. Hal ini terkait dengan pengalaman yang dialami Intel pada tahun1994. Salahsatubahasastandardalammembangunsebuahsistemdigitalatau hardware adalah VHDL. Ada beberapa tools yang bisa dilakukan untuk verifikasi formal,salahsatunyaadalahHOLtheoremprover. PenelitianinimelakukanformalisasioperasiaritmatikaVHDLdankonstruksiterkaityangdilakukandenganmenggunakan HOL Theorem Prover. Hasilnya adalah sebuah framework yang berisi formalisasi beberapa algoritma aritmatika dasar VHDL dan konstruksi terkaitnya. Framework inikemudiandapatdigunakanuntukmemverifikasimodulVHDLyang memanfaatkan aritmatika VHDL dan konstruksi terkaitnya. Kata Kunci: formalisasi, verifikasi formal, HOL Theorem Prover, aritmatika, VHDL, framework