Hardware Router's Lookup Machine and its Formal Verification

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F63839172%3A_____%2F04%3A00000300" target="_blank" >RIV/63839172:_____/04:00000300 - isvavai.cz</a>

Alternative codes found

RIV/00216305:26230/04:PU49175

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Hardware Router's Lookup Machine and its Formal Verification

Original language description

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 thelast part, the article sums up software support needed to make behavior of the accelerator equivalent to the host computer.

Czech name

Vyhledávací stroj hardwarového směrovače a jeho formální verifikace

Czech description

Článek popisuje návrh vyhledávacího stroje implementovaného v hardwarovém akcelerátoru COMBO6 pro směrování IPv4 a IPv6 paketů. Vyhledávací stroj je single instruction zařízení využívající CAM a statických pamětí. Jeho výkonnou částí je FPGA. Konvenčnímimetodami je obtížné dokázat správnost návrhu takového designu. Použili jsme metod formální verifikace (konkrétně model checking) pro ověření správnosti návrhu. Celý postup je detailně popsán. V závěru článek shrnuje podporu softwaru nutnou pro to, aby akcelerátor směroval a filtroval stejně jako hostitelský počítač.

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2004

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

ICN'2004 Conference Proceedings

ISBN

0-86341-325-0

ISSN

—

e-ISSN

—

Number of pages

6

Pages from-to

1002-1007

Publisher name

University of Haute Alsace, Colmar, France

Place of publication

Gosier, Guadeloupe, French Carribian

Event location

Gosier, Guadeloupe, French Caribbean

Event date

Feb 29, 2004

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—