Conference paper

ANTOŠ David and KOŘENEK Jan. Hardware Router's Lookup Machine and its Formal Verification. In: Proceedings of the 3rd International Conference on Networking ICN '04. Colmar: University of Haute Alsace, 2004, pp. 1002-1007. ISBN 0-86341-325-0.
Publication language:english
Original title:Hardware Router's Lookup Machine and its Formal Verification
Title (cs):Hardwarový vyhledávací stroj a jeho formální verifikace
Pages:1002-1007
Proceedings:Proceedings of the 3rd International Conference on Networking ICN '04
Conference:3rd International Conference on Networking
Place:Colmar, FR
Year:2004
ISBN:0-86341-325-0
Publisher:University of Haute Alsace
Keywords
IPv6 routing, FPGA, formal verification, Liberouter
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   author = {David Anto{\v{s}} and Jan Ko{\v{r}}enek},
   title = {Hardware Router's Lookup Machine and its Formal Verification},
   pages = {1002--1007},
   booktitle = {Proceedings of the 3rd International Conference on
	Networking ICN '04},
   year = {2004},
   location = {Colmar, FR},
   publisher = {University of Haute Alsace},
   ISBN = {0-86341-325-0},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=7511}
}

Your IPv4 address: 54.81.45.122
Switch to IPv6 connection

DNSSEC [dnssec]