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

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KRATOCHVÍLA Tomáš ŘEHÁK Vojtěch ŠAFRÁNEK David

Year of publication 2006
Type Article in Proceedings
Conference 10 years of CESNET - CESNET CONFERENCE 2006
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords formal verification; model checking; component-based hardware; FPGA
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.