Report

MATOUŠEK Petr, SMRČKA Aleš and VOJNAR Tomáš. High-level Modelling, Analysis and Verification on FPGA-based Hardware Design. Brno: CESNET National Research and Education Network, 2005.
Publication language:english
Original title:High-level Modelling, Analysis, and Verification on FPGA-based Hardware Design
Title (cs):Modelování, analýza a verifikace návrhu hardware nad FPGA
Pages:17
Place:Brno, CZ
Year:2005
Publisher:CESNET National Research and Education Network
URL:http://www.cesnet.cz/doc/techzpravy/2005/lup/ [HTML]
URL:http://www.fit.vutbr.cz/~matousp/doc/2005/lup05.pdf [PDF]
Keywords
hardware verification, timed systems, high-level modelling, formal analysis
Annotation
Implementation of network components in hardware is a trend in advanced high-speed network technologies. Incoming packets can be analysed in fast programmable cards using FPGA. Designing such a system is not easy and requires a detailed analysis. In this paper, we discuss analysis and verification of a non-trivial system-the network monitor and analyser Scampi that has been developed within the Liberouter project. The Scampi analyser is implemented in FPGA on a special add-on card. It analyses packets incoming with the speed of several Gbps. We created an abstract model of the design and verified several safety properties. Our main task was to check if there is a risk of
buffer overflow and how to set the length of buffers to prevent
this. First, we made a timed analysis by hand and then we used automated tools - model-checkers Uppaal and TReX. In the following text, we show how to model such a complex system and some results of our analysis and verification. We also propose a framework for modelling and analysis of systems where the throughput of requests, their speed, and the length of buffers are important. The proposed models can be reused when verifying and analysing of systems of the given kind.

BibTeX:
@TECHREPORT{
   author = {Petr Matou{\v{s}}ek and Ale{\v{s}} Smr{\v{c}}ka and
	Tom{\'{a}}{\v{s}} Vojnar},
   title = {High-level Modelling, Analysis, and Verification on
	FPGA-based Hardware Design},
   pages = {17},
   year = {2005},
   location = {Brno, CZ},
   publisher = {CESNET National Research and Education Network},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=7969}
}

Your IPv4 address: 54.224.43.96
Switch to IPv6 connection

DNSSEC [dnssec]