This HTML5 document contains 44 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n9http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n19http://purl.org/net/nknouf/ns/bibtex#
n17http://localhost/temp/predkladatel/
n10http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n15http://linked.opendata.cz/resource/domain/vavai/subjekt/
n14http://linked.opendata.cz/ontology/domain/vavai/
n16https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n6http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n8http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F13%3APU106310%21RIV14-MSM-26230___/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n21http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n13http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F13%3APU106310%21RIV14-MSM-26230___
rdf:type
skos:Concept n14:Vysledek
dcterms:description
The paper describes a technique for automatic generation of abstract models of memories that can be used for efficient formal verification of hardware designs. Our approach is able to handle addressing of different sizes of data, such as quad words, double words, words, or bytes, at the same time. The technique is also applicable for memories with multiple read and write ports, memories with read and write operations with zero- or single-clock delay, and it allows the memory to start with a random initial state allowing one to formally verify the given design for all initial contents of the memory. Our abstraction allows large register-files and memories to be represented in a way that dramatically reduces the state space to be explored during formal verification of microprocessor designs. The paper describes a technique for automatic generation of abstract models of memories that can be used for efficient formal verification of hardware designs. Our approach is able to handle addressing of different sizes of data, such as quad words, double words, words, or bytes, at the same time. The technique is also applicable for memories with multiple read and write ports, memories with read and write operations with zero- or single-clock delay, and it allows the memory to start with a random initial state allowing one to formally verify the given design for all initial contents of the memory. Our abstraction allows large register-files and memories to be represented in a way that dramatically reduces the state space to be explored during formal verification of microprocessor designs.
dcterms:title
An Abstraction of Multi-Port Memories with Arbitrary Addressable Units An Abstraction of Multi-Port Memories with Arbitrary Addressable Units
skos:prefLabel
An Abstraction of Multi-Port Memories with Arbitrary Addressable Units An Abstraction of Multi-Port Memories with Arbitrary Addressable Units
skos:notation
RIV/00216305:26230/13:PU106310!RIV14-MSM-26230___
n14:predkladatel
n15:orjk%3A26230
n3:aktivita
n12:S
n3:aktivity
S
n3:dodaniDat
n13:2014
n3:domaciTvurceVysledku
n10:9761985 n10:8092761 n10:1458841
n3:druhVysledku
n21:D
n3:duvernostUdaju
n7:S
n3:entitaPredkladatele
n8:predkladatel
n3:idSjednocenehoVysledku
60261
n3:idVysledku
RIV/00216305:26230/13:PU106310
n3:jazykVysledku
n20:eng
n3:klicovaSlova
memory, register file, automatic formal verification, model checking
n3:klicoveSlovo
n6:register%20file n6:automatic%20formal%20verification n6:model%20checking n6:memory
n3:kontrolniKodProRIV
[F8ADAC0CD9E9]
n3:mistoKonaniAkce
Las Palmas de Gran Canaria
n3:mistoVydani
Las Palmas de Grand Canaria
n3:nazevZdroje
Proceedings of the 14th Computer Aided Systems Theory
n3:obor
n4:JC
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:rokUplatneniVysledku
n13:2013
n3:tvurceVysledku
Smrčka, Aleš Charvát, Lukáš Vojnar, Tomáš
n3:typAkce
n9:WRD
n3:zahajeniAkce
2013-02-10+01:00
s:numberOfPages
2
n19:hasPublisher
The Universidad de Las Palmas de Gran Canaria
n16:isbn
978-84-695-6971-9
n17:organizacniJednotka
26230