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

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

Namespace Prefixes

PrefixIRI
n14http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n16http://purl.org/net/nknouf/ns/bibtex#
n13http://localhost/temp/predkladatel/
n15http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n12http://linked.opendata.cz/resource/domain/vavai/projekt/
n18http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F07%3APU70823%21RIV10-MSM-26230___/
n17http://linked.opendata.cz/ontology/domain/vavai/
n6http://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#
n4http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n21http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n8http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n7http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F07%3APU70823%21RIV10-MSM-26230___
rdf:type
skos:Concept n17:Vysledek
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, ie. 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, ie. 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 Design with Multiple Clocks in SMV Verifying VHDL Design with Multiple Clocks in SMV
skos:prefLabel
Verifying VHDL Design with Multiple Clocks in SMV Verifying VHDL Design with Multiple Clocks in SMV
skos:notation
RIV/00216305:26230/07:PU70823!RIV10-MSM-26230___
n3:aktivita
n20:Z n20:P
n3:aktivity
P(GA102/04/0780), P(GA102/05/0723), Z(MSM0021630528), Z(MSM6383917201)
n3:dodaniDat
n7:2010
n3:domaciTvurceVysledku
n15:1842919 n15:9761985 n15:1458841
n3:druhVysledku
n8:D
n3:duvernostUdaju
n19:S
n3:entitaPredkladatele
n18:predkladatel
n3:idSjednocenehoVysledku
457809
n3:idVysledku
RIV/00216305:26230/07:PU70823
n3:jazykVysledku
n21:eng
n3:klicovaSlova
model checking, hardware, VHDL, multiple clocks, SMV
n3:klicoveSlovo
n4:SMV n4:model%20checking n4:multiple%20clocks n4:VHDL n4:hardware
n3:kontrolniKodProRIV
[64BD45BDCE79]
n3:mistoKonaniAkce
Bonn
n3:mistoVydani
Bonn
n3:nazevZdroje
Formal Methods: Applications and Technology
n3:obor
n11:JC
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
6
n3:projekt
n12:GA102%2F05%2F0723 n12:GA102%2F04%2F0780
n3:rokUplatneniVysledku
n7:2007
n3:tvurceVysledku
Řehák, Vojtěch Vojnar, Tomáš Matoušek, Petr Šafránek, David Řehák, Zdeněk Smrčka, Aleš
n3:typAkce
n14:WRD
n3:zahajeniAkce
2006-08-26+02:00
n3:zamer
n6:MSM6383917201 n6:MSM0021630528
s:issn
0302-9743
s:numberOfPages
16
n16:hasPublisher
Springer-Verlag
n13:organizacniJednotka
26230