Hardware Router's Lookup Machine and its Formal Verification

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

ANTOŠ David ŘEHÁK Vojtěch KOŘENEK Jan

Year of publication 2004
Type Article in Proceedings
Conference ICN'2004 Conference Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Web http://conf.uha.fr/ICN2004.html
Field Informatics
Keywords IPv6 routing; FPGA; formal verification; Liberouter
Description This article describes the design of the lookup machine implemented in hardware accelerator COMBO6 for IPv6 and IPv4 packet routing. The lookup machine is a single instruction machine using Content Addressable and Static Memories and the operations are performed by Field Programmable Gate Arrays. The design of the lookup machine is difficult to be proven correct by conventional methods, therefore model checking as a method of formal verification was employed and this case is explained in detail. In the last part, the article sums up software support needed to make behavior of the accelerator equivalent to the host computer.
Related projects:

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