About: Verification Results in Liberouter Project     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

AttributesValues
rdf:type
rdfs:seeAlso
Description
  • 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. (cs)
  • 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.
  • 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. (en)
Title
  • Verification Results in Liberouter Project
  • Verification Results in Liberouter Project (en)
  • Výsledky verifikace v rámci projektu Liberouter (cs)
skos:prefLabel
  • Verification Results in Liberouter Project
  • Verification Results in Liberouter Project (en)
  • Výsledky verifikace v rámci projektu Liberouter (cs)
skos:notation
  • RIV/00216224:14330/04:00010306!RIV08-MSM-14330___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(GA201/03/0509), Z(MSM 000000001), Z(MSM 143300001), Z(MSM6383917201)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 592338
http://linked.open...ai/riv/idVysledku
  • RIV/00216224:14330/04:00010306
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • formal verification; programmable hardware; FPGA; Cadence SMV; VHDL; Verilog (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...i/riv/kodPristupu
http://linked.open...ontrolniKodProRIV
  • [4C7D68DA1FCF]
http://linked.open...i/riv/mistoVydani
  • Praha
http://linked.open...telVyzkumneZpravy
  • CESNET, z.s.p.o.
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Holeček, Jan
  • Šafránek, David
  • Šimeček, Pavel
  • Řehák, Vojtěch
  • Kratochvíla, Tomáš
http://linked.open...rzeVyzkumneZpravy
  • CESNET Technical Report No. 03/2004
http://linked.open...n/vavai/riv/zamer
http://localhost/t...ganizacniJednotka
  • 14330
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software