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

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

Namespace Prefixes

PrefixIRI
n19http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F10%3APU91969%21RIV12-MSM-26230___/
dctermshttp://purl.org/dc/terms/
n17http://localhost/temp/predkladatel/
n12http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n9http://linked.opendata.cz/resource/domain/vavai/projekt/
n11http://linked.opendata.cz/ontology/domain/vavai/
n16http://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/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n15http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n10http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n13http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F10%3APU91969%21RIV12-MSM-26230___
rdf:type
n11:Vysledek skos:Concept
dcterms:description
Two original approaches to formal verification of hardware designs are introduced. In particular, we aim at model checking of circuits with multiple clocks and verification of parametrized hardware designs. Considering the former contribution, we introduce four methods which we use for modelling the clock domain crossing of a circuit. Models derived in such a way can then be model checked as usual while possible problems stemming from the synchronization within a circuit are implicitly covered. Four proposed ways of modelling a data transfer differ in their precision and the incurred verification cost. In the latter contribution, our proposed approach of verification is based on a translation of parametrized hardware designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. A parametrized hardware design translated to a counter automaton can be verified for all possible values of parameters at once. Two original approaches to formal verification of hardware designs are introduced. In particular, we aim at model checking of circuits with multiple clocks and verification of parametrized hardware designs. Considering the former contribution, we introduce four methods which we use for modelling the clock domain crossing of a circuit. Models derived in such a way can then be model checked as usual while possible problems stemming from the synchronization within a circuit are implicitly covered. Four proposed ways of modelling a data transfer differ in their precision and the incurred verification cost. In the latter contribution, our proposed approach of verification is based on a translation of parametrized hardware designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. A parametrized hardware design translated to a counter automaton can be verified for all possible values of parameters at once.
dcterms:title
Verification of Asynchronous and Parametrized Hardware Designs Verification of Asynchronous and Parametrized Hardware Designs
skos:prefLabel
Verification of Asynchronous and Parametrized Hardware Designs Verification of Asynchronous and Parametrized Hardware Designs
skos:notation
RIV/00216305:26230/10:PU91969!RIV12-MSM-26230___
n3:aktivita
n15:S n15:P n15:Z
n3:aktivity
P(GAP103/10/0306), S, Z(MSM0021630528)
n3:cisloPeriodika
2
n3:dodaniDat
n13:2012
n3:domaciTvurceVysledku
n12:1458841
n3:druhVysledku
n14:J
n3:duvernostUdaju
n5:S
n3:entitaPredkladatele
n19:predkladatel
n3:idSjednocenehoVysledku
295526
n3:idVysledku
RIV/00216305:26230/10:PU91969
n3:jazykVysledku
n10:eng
n3:klicovaSlova
Formal verification, modelling hardware design, clock domain crossing, parametrized hardware design, counter automata.
n3:klicoveSlovo
n4:clock%20domain%20crossing n4:counter%20automata. n4:Formal%20verification n4:modelling%20hardware%20design n4:parametrized%20hardware%20design
n3:kodStatuVydavatele
SK - Slovenská republika
n3:kontrolniKodProRIV
[4C080C641634]
n3:nazevZdroje
Information Sciences and Technologies Bulletin of the ACM Slovakia
n3:obor
n7:JC
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
1
n3:projekt
n9:GAP103%2F10%2F0306
n3:rokUplatneniVysledku
n13:2010
n3:svazekPeriodika
2
n3:tvurceVysledku
Smrčka, Aleš
n3:zamer
n16:MSM0021630528
s:issn
1338-1237
s:numberOfPages
10
n17:organizacniJednotka
26230