Verification Results in Liberouter Project

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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
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ů