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

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F63839172%3A_____%2F05%3A00000112" target="_blank" >RIV/63839172:_____/05:00000112 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

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

Original language description

The document presents high-level modelling and formal analysis and verification on an FPGA-based multigigabit network monitoring system called Scampi. It describes an abstract model of the design and verifies several safety properties. Our main task wasto 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 (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.

Czech name

Vysokoúrovňové modelování, analýza a verifikace návrhu hardware založeného na FPGA

Czech description

Tento dokument prezentuje vysokoúrovňové modelování a formální analýzu a verifikaci miltigigabitového síťového monitorujícího systému Scampi založeném na FPGA. Popisuje abstraktní model návrhu a verifikaci některých bezpečnostních vlastností. Cílem je ověřit, jestli hrozí riziko přetečení vyrovnávacích pamětí a jak nastavit velikosti těchto pamětí. Nejprve je představena časová analýza ručně i automaticky pomocí nástrojů Uppaal a TReX, následně je ukázán postup, jak modelovat složitý systém, a jsou předvedeny výsledky analýzy a verifikace systému Scampi (propustnost a rychlost a délky vyrovnávacích pamětí). Představené modely mohou být rovněž užity při verifikaci podobných systémů.

Type

A - Audiovisual production

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2005

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

—

Place of publication

—

Publisher/client name

—

Version

8/2005

Carrier ID

—