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š; ŘEHÁK Vojtěch; VOJNAR Tomáš; ŠAFRÁNEK David; MATOUŠEK Petr; ŘEHÁK Zdeněk
• Rok publikování: 2007
• Druh: Článek ve sborníku
• Konference: 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
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: formal verification; model checking; VHDL; asynchronous clock domains
• Popis: Č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í.

Související projekty

• Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy
• Automatizovaná verifikace softwaru