Detail výsledku

Hardware Router's Lookup Machine and its Formal Verification

ANTOŠ, D.; KOŘENEK, J. Hardware Router's Lookup Machine and its Formal Verification. Proceedings of the 3rd International Conference on Networking ICN '04. Colmar: University of Haute Alsace, 2004. p. 1002-1007. ISBN: 0-86341-325-0.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Antoš David, Mgr.
Kořenek Jan, doc. Ing., Ph.D., UPSY (FIT)
Abstrakt

This article describes the design of the lookup machine implemented inhardware accelerator COMBO6 for IPv6 and IPv4 packet routing. The lookupmachine is a single instruction machine using Content Addressable andStatic Memories and the operations are performed by Field ProgrammableGate Arrays.The design of the lookup machine is difficult to be proven correct byconventional methods, therefore model checking as a method of formalverification was employed and this case is explained in detail.In the last part, the article sums up software support needed to makebehavior of the accelerator equivalent to the host computer.

Klíčová slova

IPv6 routing, FPGA, formal verification, Liberouter

Rok
2004
Strany
1002–1007
Sborník
Proceedings of the 3rd International Conference on Networking ICN '04
Konference
3rd International Conference on Networking
ISBN
0-86341-325-0
Vydavatel
University of Haute Alsace
Místo
Colmar
BibTeX 
@inproceedings{BUT17149,
  author="David {Antoš} and Jan {Kořenek}",
  title="Hardware Router's Lookup Machine and its Formal Verification",
  booktitle="Proceedings of the 3rd International Conference on Networking ICN '04",
  year="2004",
  pages="1002--1007",
  publisher="University of Haute Alsace",
  address="Colmar",
  isbn="0-86341-325-0"
}
Projekty
Optická síť národního výzkumu a její nové aplikace, MŠMT, Výzkumná centra (2000-2004), MSM6383917201, zahájení: 2004-01-01, ukončení: 2010-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina reprogramovatelných architektur (VZ FPGA)
Pracoviště
Ústav počítačových systémů (UPSY)
Nahoru