Verification Results in Liberouter Project

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Výsledky verifikace v rámci projektu Liberouter
Autoři	HOLEČEK Jan KRATOCHVÍLA Tomáš ŘEHÁK Vojtěch ŠAFRÁNEK David ŠIMEČEK Pavel
Rok publikování	2004
Druh	Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace	HOLEČEK, Jan, Tomáš KRATOCHVÍLA, Vojtěch ŘEHÁK, David ŠAFRÁNEK a Pavel ŠIMEČEK. Verification Results in Liberouter Project. Praha: CESNET, z.s.p.o., 2004. CESNET Technical Report No. 03/2004.
Popis	Tato technická zpráva popisuje naše výsledky verifikace hardwarových návrhů komponent karet Liberouter a Scampi v rámci projektu Liberouter. Používáme symbolický model checker Cadence SMV, do jehož vstupního jazyka převádíme zdrojový VHDL kód přes Verilog. Tímto způsobem jsme ověřili mnoho vlastností HW komponent.
Související projekty:	Automatizovaná verifikace paralelních a distribuovaných systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů