All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Verification of Asynchronous and Parametrized Hardware Designs

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F10%3APU90556" target="_blank" >RIV/00216305:26230/10:PU90556 - isvavai.cz</a>

  • Result on the web

  • DOI - Digital Object Identifier

Alternative languages

  • Result language

    angličtina

  • Original language name

    Verification of Asynchronous and Parametrized Hardware Designs

  • Original language 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 introducefour 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&nbsp; within a circuit are implicitly covered. Fourproposed 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 andon 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.

  • Czech name

  • Czech description

Classification

  • Type

    B - Specialist book

  • CEP classification

    IN - Informatics

  • OECD FORD branch

Result continuities

  • Project

    <a href="/en/project/GAP103%2F10%2F0306" target="_blank" >GAP103/10/0306: Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness</a><br>

  • Continuities

    Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Others

  • Publication year

    2010

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Data specific for result type

  • ISBN

    978-80-214-4214-6

  • Number of pages

    115

  • Publisher name

    Faculty of Information Technology BUT

  • Place of publication

    Brno

  • UT code for WoS book