About: Verifying VHDL Design with Multiple Clocks in SMV

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

About: Verifying VHDL Design 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, ie. 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, ie. 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 Design with Multiple Clocks in SMV Verifying VHDL Design with Multiple Clocks in SMV (en)
skos:prefLabel	Verifying VHDL Design with Multiple Clocks in SMV Verifying VHDL Design with Multiple Clocks in SMV (en)
skos:notation	RIV/00216305:26230/07:PU70823!RIV10-MSM-26230___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(GA102/04/0780), P(GA102/05/0723), Z(MSM0021630528), Z(MSM6383917201)
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš Matoušek, Petr Smrčka, Aleš
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	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	457809
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/07:PU70823
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	model checking, hardware, VHDL, multiple clocks, SMV (en)
http://linked.open.../riv/klicoveSlovo	multiple clocks VHDL model checking hardware SMV
http://linked.open...ontrolniKodProRIV	[64BD45BDCE79]
http://linked.open...v/mistoKonaniAkce	Bonn
http://linked.open...i/riv/mistoVydani	Bonn
http://linked.open...i/riv/nazevZdroje	Formal Methods: Applications and Technology
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	6 (xsd:int)
http://linked.open...vavai/riv/projekt	Automated methods and tools supporting development of reliable concurrent and distributed systems A Framework for Formal Specifications and Prototyping of Information System's Network Applications
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	2006-08-26 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti Optical National Research Network and Its New Applications
issn	0302-9743
number of pages	16 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Verifying VHDL Design with Multiple Clocks in SMV Verifying VHDL Design with Multiple Clocks in SMV Verifying VHDL Design 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, 36 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software