Detail publikace
High-level Modelling, Analysis and Verification on FPGA-based Hardware Design
Matoušek Petr, doc. Ing., Ph.D., M.A. (UIFS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
hardware verification, timed systems, high-level modelling, formal analysis
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ů.
@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/"
}