About: Verifying VHDL Designs with Multiple Clocks in SMV

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Verifying VHDL Designs with Multiple Clocks in SMV Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
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)
Title	Verifying VHDL Designs with Multiple Clocks in SMV Verifying VHDL Designs with Multiple Clocks in SMV (en)
skos:prefLabel	Verifying VHDL Designs with Multiple Clocks in SMV Verifying VHDL Designs with Multiple Clocks in SMV (en)
skos:notation	RIV/00216224:14330/07:00019329!RIV11-AV0-14330___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(1ET408050503), P(1M0545), P(GA201/06/1338), P(GD102/05/H050), Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2011
http://linked.open...aciTvurceVysledku	Smrčka, Aleš Řehák, Zdeněk Šafránek, David Vojnar, Tomáš Řehák, Vojtěch
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	457810
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/07:00019329
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	formal verification; model checking; VHDL; asynchronous clock domains (en)
http://linked.open.../riv/klicoveSlovo	VHDL model checking formal verification asynchronous clock domains
http://linked.open...ontrolniKodProRIV	[041677EE913A]
http://linked.open...v/mistoKonaniAkce	Bonn
http://linked.open...i/riv/mistoVydani	Bonn
http://linked.open...i/riv/nazevZdroje	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
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	5 (xsd:int)
http://linked.open...cetTvurcuVysledku	6 (xsd:int)
http://linked.open...vavai/riv/projekt	Automated software verification Institute for Theoretical Computer Science Integrated Approach to Education of PhD Students in the Area of Parallel and Distributed Systems Techniques for automatic verification and validation of software and hardware systems
http://linked.open...UplatneniVysledku	2007
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Šafránek, David Řehák, Zdeněk Matoušek, Petr Řehák, Vojtěch Smrčka, Aleš
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2007-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	2075-2180
number of pages	16 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-540-70951-0
http://localhost/t...ganizacniJednotka	14330
is http://linked.open...avai/riv/vysledek of	Verifying VHDL Designs with Multiple Clocks in SMV Verifying VHDL Designs with Multiple Clocks in SMV

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 41 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software