A 2003

Verification of COMBO6 VHDL Design

KRATOCHVÍLA, Tomáš, Vojtěch ŘEHÁK a Pavel ŠIMEČEK

Základní údaje

Originální název

Verification of COMBO6 VHDL Design

Autoři

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

Vydání

Praha, CESNET Technical Report No. 17/2003, 2003

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

Kód RIV

RIV/00216224:14330/03:00008325

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

Liberouter; Combo6; formal verification; hardware verification; model checking; Cadence SMV; LeonardoSpectrum
Změněno: 18. 10. 2004 15:55, doc. RNDr. Vojtěch Řehák, Ph.D.

Anotace

V originále

This technical report presents current results and experiences of the formal verification of VHDL design of Combo6 hardware accelerator card. Information about formal verification itself is enriched by description of transformation from VHDL to the Cadence SMV specification language and the system of assertions established as a compact way of communication with VHDL designers.

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ů