Hardware Router's Lookup Machine and its Formal Verification

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2004
Druh Článek ve sborníku
Konference ICN'2004 Conference Proceedings
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://conf.uha.fr/ICN2004.html
Obor Informatika
Klíčová slova IPv6 routing; FPGA; formal verification; Liberouter
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.