Verifying Parametrised Hardware Designs Via Counter Automata

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F08%3APU70924" target="_blank" >RIV/00216305:26230/08:PU70924 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Verifying Parametrised Hardware Designs Via Counter Automata

Original language description

The paper presents a new approach to formal verification of generic (i.e. parametrised) hardware designs specified in VHDL. The proposed approach is based on a translation of such designs to counter automata and on exploiting the recent advances achievedin the area of their automated formal verification. We have implemented the proposed translation. Using one of the state-of-the-art tools for verification of counter automata, we were then able to verify several non-trivial properties of parametrised VHDL components, including a real-life one.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

Confidentiality

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

Article name in the collection

Hardware and Software, Verification and Testing

ISBN

—

ISSN

0302-9743

e-ISSN

—

Number of pages

18

Pages from-to

—

Publisher name

Springer Verlag

Place of publication

Heidelberg

Event location

IBM Haifa Labs

Event date

Oct 23, 2007

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—