Attributes | Values |
---|
rdf:type
| |
Description
| - 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.
- 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. (en)
- Č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í. (cs)
|
Title
| - Verifying VHDL Designs with Multiple Clocks in SMV
- Verifikace VHDL programů s více hodinami pomocí SMV (cs)
- Verifying VHDL Designs with Multiple Clocks in SMV (en)
|
skos:prefLabel
| - Verifying VHDL Designs with Multiple Clocks in SMV
- Verifikace VHDL programů s více hodinami pomocí SMV (cs)
- Verifying VHDL Designs with Multiple Clocks in SMV (en)
|
skos:notation
| - RIV/63839172:_____/07:00000636!RIV08-MSM-63839172
|
http://linked.open.../vavai/riv/strany
| |
http://linked.open...avai/riv/aktivita
| |
http://linked.open...avai/riv/aktivity
| |
http://linked.open...iv/cisloPeriodika
| |
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/63839172:_____/07:00000636
|
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - formal verification; model checking; VHDL; asynchronous clock domains (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...odStatuVydavatele
| - DE - Spolková republika Německo
|
http://linked.open...ontrolniKodProRIV
| |
http://linked.open...i/riv/nazevZdroje
| - Lecture Notes in Computer Science
|
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...UplatneniVysledku
| |
http://linked.open...v/svazekPeriodika
| |
http://linked.open...iv/tvurceVysledku
| - Vojnar, Tomáš
- Šafránek, David
- Matoušek, Petr
- Řehák, Vojtěch
|
http://linked.open...n/vavai/riv/zamer
| |
issn
| |
number of pages
| |
is http://linked.open...avai/riv/vysledek
of | |