Hasil Pencarian  ::  Simpan CSV :: Kembali

"Pada pengembangan sistem, dibutuhkan sebuah mekanisme untuk menjamin bahwa sistem tersebut berjalan dengan benar tanpa error atau rsquo;bug rsquo;. Sejauh ini, hal yang biasa dilakukan adalah dengan testing, tetapi hal ini sulit dilakukan untuk mencakup 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 tahun 1994. Salah satu bahasa standar dalam membangun sebuah sistem digital atau hardware adalah VHDL. Ada beberapa tools yang bisa dilakukan untuk verifikasi formal, salah satunya adalah HOL theorem prover. Penelitian ini melakukan formalisasi operasi aritmatika VHDL dan konstruksi terkait yang dilakukan dengan menggunakan HOL Theorem Prover. Hasilnya adalah sebuah framework yang berisi formalisasi beberapa algoritma aritmatika dasar VHDL dan konstruksi terkaitnya. Framework ini kemudian dapat digunakan untuk memverifikasi modul VHDL yang memanfaatkan aritmatika VHDL dan konstruksi terkaitnya.

---

In system development, a mechanism is needed to ensure that the system runs correctly without error or rsquo bug rsquo . So far, testing is a common solution, but it rsquo s hard to cover all error possibilities. For systems that require a high level of correctness, such as hardware systems, there is a need for a mechanism that can ensure the correctness of the program for all possible inputs. There is another solution to do the task, i.e. by formal verification. Formal verification is done by mathematical modeling. One system that requires a high level of correctness is the floating point number system. This is related to the experience of Intel in 1994.

One of the standard languages in developing a digital system or a hardware is VHDL. There are several tools that can be used for formal verification, one of which is HOL Theorem Prover. This research conducts a formalization of VHDL arithmetic operation and the related constructions done by using HOL Theorem Prover. The result is a framework which contains the formalization of some basic VHDL arithmetic algorithms and the related constructions. This framework can then be used to verify VHDL modules that utilize the VHDL arithmetic and the related constructs."

"HOL is a theorem prover based on a higher order logic. Its expressive logic makes it suitable for embedding programming logics. Compared to other theorem provers, HOL is attractive because of its familiar and intuitive logic and because it is highly programmable. In this paper we will compare a number of commonly used embedding approaches in HOL and outline their strength and weakness. We will also outline a new alternative called hybrid embedding that combines the strength of other approaches, though some price will have to be paid. "

"Penelitian pendahuluan ini mempunyai tujuan untuk menghasilkan formalisasi sebagian dari teori graph. Graph merupakan ilmu yang cakupannya luas dan mempunyai banyak aplikasi. Akan tetapi, di dalam pustaka sistem HOL belum terdapat teori graph yang formal. Penyusunan formalisasi diawali dengan studi literatur mengenai sistem HOL, kemudian dilanjutkan dengan eksperimen-eksperimen. Terdapat enam buah eksperimen yang dilakukan secara bertahap. Eksperimen pertama berupa eksperimen menggunakan pustaka HOL. Eksperimen kedua berupa eksperimen memformalisasikan teori gcd yang kemudian memberikan pengetahuan mengenai bentuk formalisasi teori. Eksperimen ketiga menghasilkan struktur data untuk teori graph dan sebuah definisi dari teori graph. Eksperimen keempat menjelaskan beberapa contoh pembuktian menggunakan Taktik yang membantu terbentuknya formalisasi teori graph. Eksperimen kelima dan keenam memaparkan hal-hal yang perlu diperhatikan dari definisi-definisi dan teorema informal dari teori graph. Hasil dari penelitian ini adalah formalisasi dari sebagian teori graph yang dinyatakan dalam 21 definisi penting, 6 definisi umum, 28 definisi bantuan, 3 definisi tanggung, dan 1 teorema. Selain itu, dihasilkan juga pedoman pembuktian menggunakan Taktik dalam sistem HOL.This preliminary research has a goal to produce a formalization of part of graph theory. Graph has been known widely and has many applications. However, a formalization of graph theory has not been implemented in HOL system?s library. This work begins with studying literature about HOL system, then continued with several experiments. There are six experiments. The first experiment is using HOL?s library. The second experiment is formalization on GCD theory, which then elaborates the basic form of formalization. The third experiment produces data structures for graph theory and one definition of graph theory. The fourth experiment describes several proofing examples using Tactic that help make a formalization on graph theory. The fifth and sixth experiments explain things to note from the informal definitions and theorems of graph theory. The result from this research is a formalization of part of graph theory that stated in 21 important definitions, 6 general definitions, 28 helper definitions, 3 pseudo definitions, and 1 theorems. In addition, proofing guidance using Tactic in HOL system also be produced."

"Skripsi ini membahas kemampuan mahasiswa Fakultas Teknik UI angkatan 2005 dalam membuat suatu program kalkulator digital dengan menggunakan VHDL. Percobaan ini adalah percobaan kualitatif dengan desain rekayasa pemrograman. Hasil percobaan menunjukan bahwa program kalkulator dapat terselesaikan dengan mengacu kepada prinsip-prinsip digital dan pemrograman assembly. Terdapat setidaknya empat keuntungan dalam pemrograman menggunakan VHDL : spesifikasi exekusi, ketidakbergantungan pada teknologi dan peralatan, data desain yang dapat dibawa-bawa, dan mensimulasikan secara awal dan cepat.

---

The focus of this study is the freshmen student of Department of Electrical Engineering at University of Indonesia experience of making a digital calculator program by using VHDL. The result of this project shows that calculator program can be made based on digital principals and assembly programming. There are at least four benefits by programming using VHDL : executable specification, technology and tool independence, portable design data , and simulate early and fast."