Detail publikace

High-level Modelling, Analysis, and Verification on FPGA-based Hardware Design

SMRČKA, A., MATOUŠEK, P., VOJNAR, T.

Originální název

High-level Modelling, Analysis, and Verification on FPGA-based Hardware Design

Typ

konferenční sborník (ne článek)

Jazyk

angličtina

Originální abstrakt

Implementation of network components in hardware is a trend in advancedhigh-speed network technologies. Incoming packets can be analysed infast programmable cards using FPGA. Designing such a system is not easyand requires a detailed analysis. In this paper, we discuss analysisand verification of a non-trivial system-the network monitor andanalyser Scampi that has been developed within the Liberouter project.The Scampi analyser is implemented in FPGA on a special add-on card. Itanalyses packets incoming with the speed of several Gbps. We created anabstract 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 usedautomated tools - model-checkers Uppaal and TReX. In the followingtext, we show how to model such a complex system and some results ofour analysis and verification. We also propose a framework formodelling and analysis of systems where the throughput of requests,their speed, and the length of buffers are important. The proposedmodels can be reused when verifying and analysing of systems of thegiven kind.

Klíčová slova

hardware verification, timed systems, high-level modelling, formal analysis

Autoři

SMRČKA, A., MATOUŠEK, P., VOJNAR, T.

Rok RIV

2005

Vydáno

11. 11. 2005

Nakladatel

CESNET National Research and Education Network

Místo

Brno

Strany počet

17

URL

http://www.fit.vutbr.cz/~matousp/doc/2005/lup05.pdf, http://www.cesnet.cz/doc/techzpravy/2005/lup/

BibTex

@proceedings{BUT57593,
  editor="Aleš {Smrčka} and Petr {Matoušek} and Tomáš {Vojnar}",
  title="High-level Modelling, Analysis, and Verification on FPGA-based Hardware Design",
  year="2005",
  pages="17",
  publisher="CESNET National Research and Education Network",
  address="Brno",
  url="http://www.fit.vutbr.cz/~matousp/doc/2005/lup05.pdf, http://www.cesnet.cz/doc/techzpravy/2005/lup/"
}