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.
|