2004
Hardware Router's Lookup Machine and its Formal Verification
ANTOŠ, David; Vojtěch ŘEHÁK and Jan KOŘENEKBasic information
Original name
Hardware Router's Lookup Machine and its Formal Verification
Authors
ANTOŠ, David; Vojtěch ŘEHÁK and Jan KOŘENEK
Edition
Gosier, Guadeloupe, French Caribbean, ICN'2004 Conference Proceedings, p. 1002-1007, 6 pp. 2004
Publisher
University of Haute Alsace, Colmar, France
Other information
Language
English
Type of outcome
Proceedings paper
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Guadeloupe
Confidentiality degree
is not subject to a state or trade secret
References:
Organization unit
Faculty of Informatics
ISBN
0-86341-325-0
Keywords in English
IPv6 routing; FPGA; formal verification; Liberouter
Changed: 13/1/2005 11:00, RNDr. David Antoš, Ph.D.
Abstract
In the original language
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.
Links
| GA201/03/0509, research and development project |
| ||
| MSM 000000001, plan (intention) |
| ||
| MSM 143300001, plan (intention) |
|