Verifying VHDL Designs with Multiple Clocks in SMV

SMRČKA, Aleš, Vojtěch ŘEHÁK, Tomáš VOJNAR, David ŠAFRÁNEK, Petr MATOUŠEK and Zdeněk ŘEHÁK. Verifying VHDL Designs with Multiple Clocks in SMV. In Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006. Bonn: Springer-Verlag, 2007, p. 148-164, 16 pp. ISBN 978-3-540-70951-0.

Basic information

Original name

Verifying VHDL Designs with Multiple Clocks in SMV

Name in Czech

Verifikace VHDL programů s více hodinami pomocí SMV

Authors

SMRČKA, Aleš (203 Czech Republic), Vojtěch ŘEHÁK (203 Czech Republic), Tomáš VOJNAR (203 Czech Republic), David ŠAFRÁNEK (203 Czech Republic, guarantor), Petr MATOUŠEK (203 Czech Republic) and Zdeněk ŘEHÁK (203 Czech Republic)

Edition

Bonn, Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, p. 148-164, 16 pp. 2007

Publisher

Springer-Verlag

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/07:00019329

Organization unit

Faculty of Informatics

ISBN

978-3-540-70951-0

ISSN

UT WoS

000245773800010

Keywords in English

formal verification; model checking; VHDL; asynchronous clock domains

Tags

asynchronous clock domains, formal verification, Model checking, VHDL

Tags

International impact, Reviewed

---

Abstract

V originále

The paper considers the problem of model checking real-life VHDL- based hardware designs via their automated transformation to a model verifiable using the SMV model checker. In particular, model checking of asynchronous designs, i.e. designs driven by multiple clocks, is discussed. Two original approaches to compiling asynchronous VHDL designs to the SMV language such that errors possibly arising from the asynchronicity are preserved are proposed. The paper also presents results of experiments with using the proposed methods for verification of several real-life asynchronous components of an FPGA-based router being developed within the Liberouter project.

In Czech

Článek se zabývá problémem ověřování modelů reálných hardwarových systémů specifikovaných pomocí jazyka VHDL. Způsob verifikace je založen na překladu VHDL programů do jazyka Cadence SMV. Výsledky uvedené v tomto článku se zaměřují na reálnou verifikaci hardwarových obvodů s asynchronními komponentami. Článek uvádí dva přístupy včetně experimentálního ověření.

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science