Článek ve sborníku konference

CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. In: Proceedings of the 14th Computer Aided Systems Theory. Las Palmas de Grand Canaria: Universidad de Las Palmas de Gran Canaria, 2013, s. 254-255. ISBN 978-84-695-6971-9.
Jazyk publikace:angličtina
Název publikace:An Abstraction of Multi-Port Memories with Arbitrary Addressable Units
Název (cs):Abstrakce víceportových pamětí s obecnou velikostí adresovatelných jednotek
Strany:254-255
Sborník:Proceedings of the 14th Computer Aided Systems Theory
Konference:Fourteenth International Conference On Computer Aided Systems Theory
Místo vydání:Las Palmas de Grand Canaria, ES
Rok:2013
ISBN:978-84-695-6971-9
Vydavatel:Universidad de Las Palmas de Gran Canaria
Soubory: 
+Typ Jméno Název Vel. Poslední změna
iconeurocast13-abstract.pdf102 KB2013-01-22 15:05:35
^ Vybrat vše
S vybranými:
Klíčová slova
memory, register file, automatic formal verification, model checking
Anotace
Článek popisuje přístup pro automatické generování abstraktních modelů pamětí, které mohou být využity pro efektivní verifikaci hardware. Prezentovaný přístup uvažuje možnost adresování dat o různých velikostech jako jsou např. slabiky, slova nebo dvojslova. Technika je také použitelná pro paměti s více čtecími a zápisovými porty, paměti s nulovým nebo jednotkovým zpožděním zápisu či čtení a umožňuje modelovat paměť s náhodným počátečním stavem, čímž je docíleno možnosti verifikovat daný návrh pro všechny možné počáteční konfigurace paměti. Popsaná abstrakce umožňuje modelovat rozměrná registrová pole a paměti takovým způsobem, který významně redukuje stavový prostor, jež je prohledáván v průběhu verifikace.
Abstrakt
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 abstraction allows large register-files and memories to be represented in a way that dramatically reduces the state space to be explored during the verification.
BibTeX:
@INPROCEEDINGS{
   author = {Luk{\'{a}}{\v{s}} Charv{\'{a}}t and Ale{\v{s}} Smr{\v{c}}ka
	and Tom{\'{a}}{\v{s}} Vojnar},
   title = {An Abstraction of Multi-Port Memories with Arbitrary
	Addressable Units},
   pages = {254--255},
   booktitle = {Proceedings of the 14th Computer Aided Systems Theory},
   year = {2013},
   location = {Las Palmas de Grand Canaria, ES},
   publisher = {The Universidad de Las Palmas de Gran Canaria},
   ISBN = {978-84-695-6971-9},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs.iso-8859-2?id=10246}
}

Vaše IPv4 adresa: 54.198.108.19
Přepnout na IPv6 spojení

DNSSEC [dnssec]