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í jakospecializovaný hardware postavený nad programovatelnými poli FPGA.Vytvoření návrhu není jednoduché a vyžaduje podrobnou analýzunávrhu. V této technické zprávě ukazujeme analýzu a verifikacinetriviálního systému - síťového analyzátoru Scampi, který byl vyvíjenv rámci projektu Liberouter. Analyzátor Scampi je implementován na FPGAna 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í typubezpečnost. Měli jsme zjistit, zda mohou přetéci navržené buffery a jaknastavit jejich délku, aby k tomu nedošlo. Nejprve jsme systémanalyzovali ručně a posléze i pomocí automatizovaných nástrojů -využili jsme model checker Uppaal a TReX. V textu popisujemezpůsob, jak modelovat komplexní systémy a naše výsledky analýzy averifikace. Součástí projektu je návrh obecného rámce pro modelování a analýzusysté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/"
}