Verification Results in Liberouter Project

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.

Základní údaje

Originální název

Verification Results in Liberouter Project

Název česky

Výsledky verifikace v rámci projektu Liberouter

Autoři

HOLEČEK, Jan (203 Česká republika), Tomáš KRATOCHVÍLA (203 Česká republika), Vojtěch ŘEHÁK (203 Česká republika), David ŠAFRÁNEK (203 Česká republika, garant) a Pavel ŠIMEČEK (203 Česká republika)

Vydání

Praha, CESNET Technical Report No. 03/2004, 2004

Nakladatel

CESNET, z.s.p.o.

---

Další údaje

Jazyk

angličtina

Typ výsledku

Audiovizuální tvorba

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Kód RIV

RIV/00216224:14330/04:00010306

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

formal verification; programmable hardware; FPGA; Cadence SMV; VHDL; Verilog

Štítky

Cadence SMV, formal verification, FPGA, programmable hardware, Verilog, VHDL

---

Anotace

V originále

This technical report presents current results of the formal verification of VHDL design of Liberouter and Scampi hardware accelerator card for packet routing, originating from the Liberouter project. We use the symbolic model checker Cadence SMV to prove desired properties of separate units of the design. We have verified many properties of the number of units. Moreover, we have also gained precious experiences concerning the fight with the state explosion problem.

Česky

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.

---

Návaznosti

GA201/03/0509, projekt VaV	Název: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 000000001, záměr	Název: Vysokorychlostní síť národního výzkumu a její nové aplikace
MSM 143300001, záměr	Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů