Formal Verification of a FIFO Component in Design of Network Monitoring Hardware

KRATOCHVÍLA, Tomáš, Vojtěch ŘEHÁK and David ŠAFRÁNEK. Formal Verification of a FIFO Component in Design of Network Monitoring Hardware. In 10 years of CESNET - CESNET CONFERENCE 2006. Praha: CESNET, z.s.p.o., 2006, p. 151-160. ISBN 978-80-239-6533-9.

Basic information

Original name

Formal Verification of a FIFO Component in Design of Network Monitoring Hardware

Name in Czech

Formální verifikace FIFO komponenty při návrhu síťového monitorovacího hardware

Authors

KRATOCHVÍLA, Tomáš (203 Czech Republic), Vojtěch ŘEHÁK (203 Czech Republic) and David ŠAFRÁNEK (203 Czech Republic, guarantor)

Edition

Praha, 10 years of CESNET - CESNET CONFERENCE 2006, p. 151-160, 10 pp. 2006

Publisher

CESNET, z.s.p.o.

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/06:00015311

Organization unit

Faculty of Informatics

ISBN

978-80-239-6533-9

UT WoS

000271027200015

Keywords in English

formal verification; model checking; component-based hardware; FPGA

Tags

component-based hardware, formal verification, FPGA, Model checking

Tags

International impact, Reviewed

---

Abstract

V originále

The paper presents our approach of using a formal verification method, the model checking, to verify whether a particular component of hardware design matches its specification. We have applied this approach in the Liberouter project, which is aimed to develop an FPGA based high-speed network monitoring and routing hardware. In the paper, we focus on a FIFO component - the process of its verification, detected errors, and the way of their correction.

In Czech

V článku je prezentován specifický přístup použití formální metody ověřování modelů při verifikaci hardwarové implementace komponenty FIFO. Tento přístup byl aplikován při verifikaci klíčových hardwarových komponent v rámci projektu Liberouter. Cílem projektu Liberouter je vývoj hardwarově akcelerovaného síťového směrovače a monitorovací jednotky. Článek se zaměřuje na proces verifikace komponenty FIFO, popis odhalených chyb a způsob jejich opravy.

---

Links

GA201/03/0509, research and development project	Name: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science