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)

AttributesValues
rdf:type
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. (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:PU90556!RIV12-GA0-26230___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(GAP103/10/0306), S, Z(MSM0021630528)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 295527
http://linked.open...ai/riv/idVysledku
  • RIV/00216305:26230/10:PU90556
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • Formal verification, modelling hardware design, clock domain crossing, parametrized hardware design, counter automata. (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [675DDCDB25EB]
http://linked.open...i/riv/mistoVydani
  • Brno
http://linked.open...vEdiceCisloSvazku
  • FIT Monograph
http://linked.open...i/riv/nazevZdroje
  • Verification of Asynchronous and Parametrized Hardware Designs
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...v/pocetStranKnihy
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Vojnar, Tomáš
  • Smrčka, Aleš
http://linked.open...n/vavai/riv/zamer
number of pages
http://purl.org/ne...btex#hasPublisher
  • Vysoké učení technické v Brně. Fakulta informačních technologií
https://schema.org/isbn
  • 978-80-214-4214-6
http://localhost/t...ganizacniJednotka
  • 26230
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
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