Další formáty:
BibTeX
LaTeX
RIS
@misc{490367,
author = {Kratochvíla, Tomáš and Řehák, Vojtěch and Šimeček, Pavel},
address = {Praha},
keywords = {Liberouter; Combo6; formal verification; hardware verification; model checking; Cadence SMV; LeonardoSpectrum},
language = {eng},
location = {Praha},
publisher = {CESNET, z.s.p.o.},
title = {Verification of COMBO6 VHDL Design},
url = {http://www.cesnet.cz/doc/techzpravy/2003/translationver/},
year = {2003}
}
TY - GEN
ID - 490367
AU - Kratochvíla, Tomáš - Řehák, Vojtěch - Šimeček, Pavel
PY - 2003
TI - Verification of COMBO6 VHDL Design
VL - CESNET Technical Report No. 17/2003
PB - CESNET, z.s.p.o.
CY - Praha
KW - Liberouter
KW - Combo6
KW - formal verification
KW - hardware verification
KW - model checking
KW - Cadence SMV
KW - LeonardoSpectrum
UR - http://www.cesnet.cz/doc/techzpravy/2003/translationver/
L2 - http://www.cesnet.cz/doc/techzpravy/2003/translationver/
N2 - 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.
ER -
KRATOCHVÍLA, Tomáš, Vojtěch ŘEHÁK a Pavel ŠIMEČEK. \textit{Verification of COMBO6 VHDL Design}. Praha: CESNET, z.s.p.o. CESNET Technical Report No. 17/2003. 2003.
|
