Informační systém Masarykovy univerzity 

Verifying VHDL Designs with Multiple Clocks in SMV

česky | in English

SMRČKA, Aleš, Vojtěch ŘEHÁK, Tomáš VOJNAR, David ŠAFRÁNEK, Petr MATOUŠEK a 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. s. 148-164, 16 s. ISBN 978-3-540-70951-0.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Verifying VHDL Designs with Multiple Clocks in SMV
Název česky Verifikace VHDL programů s více hodinami pomocí SMV
Autoři SMRČKA, Aleš (203 Česká republika), Vojtěch ŘEHÁK (203 Česká republika), Tomáš VOJNAR (203 Česká republika), David ŠAFRÁNEK (203 Česká republika, garant), Petr MATOUŠEK (203 Česká republika) a Zdeněk ŘEHÁK (203 Česká republika).
Vydání 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, od s. 148-164, 16 s. 2007.
Nakladatel Springer-Verlag
Další údaje
Originální jazyk angličtina
Typ výsledku Článek ve sborníku
Obor Informatika
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/07:00019329
Organizační jednotka Fakulta informatiky
ISBN 978-3-540-70951-0
ISSN 2075-2180
UT WoS 000245773800010
Klíčová slova anglicky formal verification; model checking; VHDL; asynchronous clock domains
Štítky asynchronous clock domains, formal verification, Model checking, VHDL
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. David Šafránek, Ph.D., učo 3159. Změněno: 9. 4. 2010 16:10.
Anotace
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.
Anotace česky
Č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í.
Návaznosti
GA201/06/1338, projekt VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Doktorské granty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 23. 11. 2017 06:27

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 23. 11. 2017 06:27, 47. (lichý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému