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

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

A - Audiovizuální tvorba

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2005

Kód důvěrnosti údajů

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

ISBN

—

Místo vydání

—

Název nakladatele resp. objednatele

—

Verze

8/2005

Identifikační číslo nosiče

—