This HTML5 document contains 55 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n17http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n18http://purl.org/net/nknouf/ns/bibtex#
n21http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F07%3A00019329%21RIV11-AV0-14330___/
n10http://localhost/temp/predkladatel/
n6http://linked.opendata.cz/resource/domain/vavai/projekt/
n4http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n9http://linked.opendata.cz/ontology/domain/vavai/
n20https://schema.org/
n12http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n14http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n22http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n5http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F07%3A00019329%21RIV11-AV0-14330___
rdf:type
n9:Vysledek skos:Concept
dcterms:description
The paper considers the problem of model checking real-life VHDL- based hardware designs via their automated transformation to a model verifiable using the SMV model checker. In particular, model checking of asynchronous designs, i.e. designs driven by multiple clocks, is discussed. Two original approaches to compiling asynchronous VHDL designs to the SMV language such that errors possibly arising from the asynchronicity are preserved are proposed. The paper also presents results of experiments with using the proposed methods for verification of several real-life asynchronous components of an FPGA-based router being developed within the Liberouter project. The paper considers the problem of model checking real-life VHDL- based hardware designs via their automated transformation to a model verifiable using the SMV model checker. In particular, model checking of asynchronous designs, i.e. designs driven by multiple clocks, is discussed. Two original approaches to compiling asynchronous VHDL designs to the SMV language such that errors possibly arising from the asynchronicity are preserved are proposed. The paper also presents results of experiments with using the proposed methods for verification of several real-life asynchronous components of an FPGA-based router being developed within the Liberouter project.
dcterms:title
Verifying VHDL Designs with Multiple Clocks in SMV Verifying VHDL Designs with Multiple Clocks in SMV
skos:prefLabel
Verifying VHDL Designs with Multiple Clocks in SMV Verifying VHDL Designs with Multiple Clocks in SMV
skos:notation
RIV/00216224:14330/07:00019329!RIV11-AV0-14330___
n3:aktivita
n11:P n11:Z
n3:aktivity
P(1ET408050503), P(1M0545), P(GA201/06/1338), P(GD102/05/H050), Z(MSM0021622419)
n3:dodaniDat
n5:2011
n3:domaciTvurceVysledku
n4:9761985 n4:8225400 n4:8986371 n4:9901809 n4:1848925
n3:druhVysledku
n19:D
n3:duvernostUdaju
n15:S
n3:entitaPredkladatele
n21:predkladatel
n3:idSjednocenehoVysledku
457810
n3:idVysledku
RIV/00216224:14330/07:00019329
n3:jazykVysledku
n22:eng
n3:klicovaSlova
formal verification; model checking; VHDL; asynchronous clock domains
n3:klicoveSlovo
n14:formal%20verification n14:model%20checking n14:asynchronous%20clock%20domains n14:VHDL
n3:kontrolniKodProRIV
[041677EE913A]
n3:mistoKonaniAkce
Bonn
n3:mistoVydani
Bonn
n3:nazevZdroje
Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006
n3:obor
n13:IN
n3:pocetDomacichTvurcuVysledku
5
n3:pocetTvurcuVysledku
6
n3:projekt
n6:1M0545 n6:1ET408050503 n6:GD102%2F05%2FH050 n6:GA201%2F06%2F1338
n3:rokUplatneniVysledku
n5:2007
n3:tvurceVysledku
Řehák, Vojtěch Šafránek, David Matoušek, Petr Řehák, Zdeněk Vojnar, Tomáš Smrčka, Aleš
n3:typAkce
n17:WRD
n3:zahajeniAkce
2007-01-01+01:00
n3:zamer
n12:MSM0021622419
s:issn
2075-2180
s:numberOfPages
16
n18:hasPublisher
Springer-Verlag
n20:isbn
978-3-540-70951-0
n10:organizacniJednotka
14330