Sciweavers

HVC
2007
Springer

Verifying Parametrised Hardware Designs Via Counter Automata

13 years 9 months ago
Verifying Parametrised Hardware Designs Via Counter Automata
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 achieved in 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.
Ales Smrcka, Tomás Vojnar
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where HVC
Authors Ales Smrcka, Tomás Vojnar
Comments (0)