Publication Details

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.
Czech title
Hardwarový vyhledávací stroj a jeho formální verifikace
Type
conference paper
Language
English
Authors
Antoš David, Mgr.
Kořenek Jan, doc. Ing., Ph.D. (DCSY)
Keywords

IPv6 routing, FPGA, formal verification, Liberouter

Abstract

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.

Published
2004
Pages
1002–1007
Proceedings
Proceedings of the 3rd International Conference on Networking ICN '04
ISBN
0-86341-325-0
Publisher
University of Haute Alsace
Place
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"
}
Back to top