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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/07:00019329
Organization unit Faculty of Informatics
ISBN 978-3-540-70951-0
ISSN 2075-2180
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
Changed by Changed by: doc. RNDr. David Šafránek, Ph.D., učo 3159. Changed: 9/4/2010 16:10.
Abstract
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.
Abstract (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 projectName: Automatizovaná verifikace softwaru
Investor: Czech Science Foundation, Standard Projects
GD102/05/H050, research and development projectName: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Doctor grants
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
1ET408050503, research and development projectName: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Academy of Sciences of the Czech Republic, Information society (National programme of research)
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Research Centres (National Research Programme)
PrintDisplayed: 27/9/2020 10:34