About: Verification of Asynchronous and Parametrized Hardware Designs

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Verification of Asynchronous and Parametrized Hardware Designs 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)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
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. (en)
Title	Verification of Asynchronous and Parametrized Hardware Designs Verification of Asynchronous and Parametrized Hardware Designs (en)
skos:prefLabel	Verification of Asynchronous and Parametrized Hardware Designs Verification of Asynchronous and Parametrized Hardware Designs (en)
skos:notation	RIV/00216305:26230/10:PU91969!RIV12-MSM-26230___
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(GAP103/10/0306), S, Z(MSM0021630528)
http://linked.open...iv/cisloPeriodika	2
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Smrčka, Aleš
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	295526
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/10:PU91969
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Formal verification, modelling hardware design, clock domain crossing, parametrized hardware design, counter automata. (en)
http://linked.open.../riv/klicoveSlovo	Formal verification clock domain crossing counter automata. modelling hardware design parametrized hardware design
http://linked.open...odStatuVydavatele	SK - Slovenská republika
http://linked.open...ontrolniKodProRIV	[4C080C641634]
http://linked.open...i/riv/nazevZdroje	Information Sciences and Technologies Bulletin of the ACM Slovakia
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	1 (xsd:int)
http://linked.open...vavai/riv/projekt	Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness
http://linked.open...UplatneniVysledku	2010
http://linked.open...v/svazekPeriodika	2
http://linked.open...iv/tvurceVysledku	Smrčka, Aleš
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
issn	1338-1237
number of pages	10 (xsd:int)
http://localhost/t...ganizacniJednotka	26230

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

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, 77 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software