Publication result detail

Hardware Router's Lookup Machine and its Formal Verification

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

Original Title

Hardware Router's Lookup Machine and its Formal Verification

English Title

Hardware Router's Lookup Machine and its Formal Verification

Type

Paper in proceedings outside WoS and Scopus

Original Abstract

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.

English abstract

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.

Keywords

IPv6 routing, FPGA, formal verification, Liberouter

Key words in English

IPv6 routing, FPGA, formal verification, Liberouter

Authors

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

Released

24.06.2004

Publisher

University of Haute Alsace

Location

Colmar

ISBN

0-86341-325-0

Book

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

Pages from

1002

Pages to

1007

Pages count

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