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

Tomas Kratochvila, Vojtech Rehak, David Safranek

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.