Detail publikace

Hardware Router's Lookup Machine and its Formal Verification

ANTOŠ, D., KOŘENEK, J.

Originální název

Hardware Router's Lookup Machine and its Formal Verification

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

IPv6 routing, FPGA, formal verification, Liberouter

Autoři

ANTOŠ, D., KOŘENEK, J.

Vydáno

24. 6. 2004

Nakladatel

University of Haute Alsace

Místo

Colmar

ISBN

0-86341-325-0

Kniha

Proceedings of the 3rd International Conference on Networking ICN '04

Strany od

1002

Strany do

1007

Strany počet

6

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"
}