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 R the process of its verification, detected errors, and the way of their correction.