D 2004

Hardware Router's Lookup Machine and its Formal Verification

ANTOŠ, David, Vojtěch ŘEHÁK a Jan KOŘENEK

Základní údaje

Originální název

Hardware Router's Lookup Machine and its Formal Verification

Autoři

Vydání

Gosier, Guadeloupe, French Caribbean, ICN'2004 Conference Proceedings, od s. 1002-1007, 6 s. 2004

Nakladatel

University of Haute Alsace, Colmar, France

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Guadeloupe

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Organizační jednotka

Fakulta informatiky

ISBN

0-86341-325-0

Klíčová slova anglicky

IPv6 routing; FPGA; formal verification; Liberouter

Štítky

Změněno: 13. 1. 2005 11:00, RNDr. David Antoš, Ph.D.

Anotace

V originále

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.

Návaznosti

GA201/03/0509, projekt VaV
Název: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 000000001, záměr
Název: Vysokorychlostní síť národního výzkumu a její nové aplikace
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů