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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F10%3APU90556%21RIV12-GA0-26230___
rdf:type
n16:Vysledek skos:Concept
dcterms:description
We introduce two original approaches to formal verification of hardware designs. 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. We introduce two original approaches to formal verification of hardware designs. 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:PU90556!RIV12-GA0-26230___
n3:aktivita
n8:Z n8:S n8:P
n3:aktivity
P(GAP103/10/0306), S, Z(MSM0021630528)
n3:dodaniDat
n5:2012
n3:domaciTvurceVysledku
n9:9761985 n9:1458841
n3:druhVysledku
n17:B
n3:duvernostUdaju
n7:S
n3:entitaPredkladatele
n13:predkladatel
n3:idSjednocenehoVysledku
295527
n3:idVysledku
RIV/00216305:26230/10:PU90556
n3:jazykVysledku
n14:eng
n3:klicovaSlova
Formal verification, modelling hardware design, clock domain crossing, parametrized hardware design, counter automata.
n3:klicoveSlovo
n4:counter%20automata. n4:modelling%20hardware%20design n4:Formal%20verification n4:clock%20domain%20crossing n4:parametrized%20hardware%20design
n3:kontrolniKodProRIV
[675DDCDB25EB]
n3:mistoVydani
Brno
n3:nazevEdiceCisloSvazku
FIT Monograph
n3:nazevZdroje
Verification of Asynchronous and Parametrized Hardware Designs
n3:obor
n15:IN
n3:pocetDomacichTvurcuVysledku
2
n3:pocetStranKnihy
115
n3:pocetTvurcuVysledku
2
n3:projekt
n10:GAP103%2F10%2F0306
n3:rokUplatneniVysledku
n5:2010
n3:tvurceVysledku
Vojnar, Tomáš Smrčka, Aleš
n3:zamer
n18:MSM0021630528
s:numberOfPages
115
n19:hasPublisher
Vysoké učení technické v Brně. Fakulta informačních technologií
n21:isbn
978-80-214-4214-6
n20:organizacniJednotka
26230