Detail publikace
High-level Modelling, Analysis, and Verification on FPGA-based Hardware Design
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Síťové prvky vysokorychlostních sítí se dnes implementují jako specializovaný hardware postavený nad programovatelnými poli FPGA. Vytvoření návrhu není jednoduché a vyžaduje podrobnou analýzu návrhu. V této technické zprávě ukazujeme analýzu a verifikaci netriviálního systému - síťového analyzátoru Scampi, který byl vyvíjen v rámci projektu Liberouter. Analyzátor Scampi je implementován na FPGA na speciální kartě v počítači. Analyzuje pakety přicházející na rychlostech Gb/s.
Popisujeme zde tvorbu abstraktního modelu návrhu a ověřování vlastností typu bezpečnost. Měli jsme zjistit, zda mohou přetéci navržené buffery a jak nastavit jejich délku, aby k tomu nedošlo. Nejprve jsme systém analyzovali ručně a posléze i pomocí automatizovaných nástrojů - využili jsme model checker Uppaal a TReX. V textu popisujeme způsob, jak modelovat komplexní systémy a naše výsledky analýzy a verifikace. Součástí projektu je návrh obecného rámce pro modelování a analýzu systémů, ve kterých je kritická propustnost, rychlost a velikost bufferů. Navržený obecný rámec může být využit při analýze a verifikaci dalších systémů.
@TECHREPORT{FITPUB7969,
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 = "https://www.fit.vut.cz/research/publication/7969"
}