Other formats:
BibTeX
LaTeX
RIS
@misc{558042,
author = {Holeček, Jan and Kratochvíla, Tomáš and Řehák, Vojtěch and Šafránek, David and Šimeček, Pavel},
address = {Praha},
keywords = {formal verification; programmable hardware; FPGA; Cadence SMV; VHDL; Verilog},
language = {eng},
location = {Praha},
publisher = {CESNET, z.s.p.o.},
title = {Verification Results in Liberouter Project},
url = {http://www.cesnet.cz/doc/techzpravy/2004/verificationresults/},
year = {2004}
}
TY - GEN
ID - 558042
AU - Holeček, Jan - Kratochvíla, Tomáš - Řehák, Vojtěch - Šafránek, David - Šimeček, Pavel
PY - 2004
TI - Verification Results in Liberouter Project
VL - CESNET Technical Report No. 03/2004
PB - CESNET, z.s.p.o.
CY - Praha
KW - formal verification
KW - programmable hardware
KW - FPGA
KW - Cadence SMV
KW - VHDL
KW - Verilog
UR - http://www.cesnet.cz/doc/techzpravy/2004/verificationresults/
L2 - http://www.cesnet.cz/doc/techzpravy/2004/verificationresults/
N2 - 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.
ER -
HOLEČEK, Jan, Tomáš KRATOCHVÍLA, Vojtěch ŘEHÁK, David ŠAFRÁNEK and Pavel ŠIMEČEK. \textit{Verification Results in Liberouter Project}. Praha: CESNET, z.s.p.o., 2004. CESNET Technical Report No. 03/2004.
|
