"1002-1007" . . "2"^^ . . "Gosier, Guadeloupe" . . . "[E244B748D881]" . . "0-86341-325-0" . "1"^^ . . "Proceedings of the 3rd International Conference on Networking ICN '04" . . . "Hardwarov\u00FD vyhled\u00E1vac\u00ED stroj a jeho form\u00E1ln\u00ED verifikace"@cs . "565930" . "RIV/00216305:26230/04:PU49175" . "Hardware Router's Lookup Machine and its Formal Verification"@en . . "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 thee last part, the article sums up software support needed to make behavior of the accelerator equivalent to the host computer." . "Hardware Router's Lookup Machine and its Formal Verification"@en . . . "Hardwarov\u00FD vyhled\u00E1vac\u00ED stroj a jeho form\u00E1ln\u00ED verifikace"@cs . "6"^^ . "Ko\u0159enek, Jan" . "Colmar" . "RIV/00216305:26230/04:PU49175!RIV06-MSM-26230___" . "Hardware Router's Lookup Machine and its Formal Verification" . . "26230" . "Anto\u0161, David" . "IPv6 routing, FPGA, formal verification, Liberouter"@en . . "University of Haute Alsace" . . . "Hardware Router's Lookup Machine and its Formal Verification" . "Tento \u010Dl\u00E1nek popisuje n\u00E1vhr vyhled\u00E1vac\u00EDho stroje implementovan\u00E9ho v hardwarov\u00E9m akceler\u00E1toru COMBO6 pro IPv6 a IPv4 sm\u011Brov\u00E1n\u00ED.
"@cs . "2004-02-29+01:00"^^ . . "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 thee last part, the article sums up software support needed to make behavior of the accelerator equivalent to the host computer."@en . "Z(MSM6383917201)" . .