Other formats:
BibTeX
LaTeX
RIS
@inproceedings{493216,
author = {Antoš, David and Řehák, Vojtěch and Kořenek, Jan},
address = {Gosier, Guadeloupe, French Caribbean},
booktitle = {ICN'2004 Conference Proceedings},
keywords = {IPv6 routing; FPGA; formal verification; Liberouter},
language = {eng},
location = {Gosier, Guadeloupe, French Caribbean},
isbn = {0-86341-325-0},
pages = {1002-1007},
publisher = {University of Haute Alsace, Colmar, France},
title = {Hardware Router's Lookup Machine and its Formal Verification},
url = {http://conf.uha.fr/ICN2004.html},
year = {2004}
}
TY - JOUR
ID - 493216
AU - Antoš, David - Řehák, Vojtěch - Kořenek, Jan
PY - 2004
TI - Hardware Router's Lookup Machine and its Formal Verification
PB - University of Haute Alsace, Colmar, France
CY - Gosier, Guadeloupe, French Caribbean
SN - 0863413250
KW - IPv6 routing
KW - FPGA
KW - formal verification
KW - Liberouter
UR - http://conf.uha.fr/ICN2004.html
N2 - 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.
ER -
ANTOŠ, David, Vojtěch ŘEHÁK and Jan KOŘENEK. Hardware Router's Lookup Machine and its Formal Verification. In \textit{ICN'2004 Conference Proceedings}. Gosier, Guadeloupe, French Caribbean: University of Haute Alsace, Colmar, France, 2004, p.~1002-1007. ISBN~0-86341-325-0.
|
