Conference paper

CHARVÁT Lukáš, SMRČKA Aleš and 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: The Universidad de Las Palmas de Gran Canaria, 2013, pp. 254-255. ISBN 978-84-695-6971-9.
Publication language:english
Original title:An Abstraction of Multi-Port Memories with Arbitrary Addressable Units
Title (cs):Abstrakce víceportových pamětí s obecnou velikostí adresovatelných jednotek
Pages:254-255
Proceedings:Proceedings of the 14th Computer Aided Systems Theory
Conference:Fourteenth International Conference On Computer Aided Systems Theory
Place:Las Palmas de Grand Canaria, ES
Year:2013
ISBN:978-84-695-6971-9
Publisher:The Universidad de Las Palmas de Gran Canaria
Files: 
+Type Name Title Size +Last modified
iconeurocast13-abstract.pdf102 KB2013-01-22 15:05:35
^ Select all
With selected:
Keywords
memory, register file, automatic formal verification, model checking
Annotation
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.
Abstract
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.en.iso-8859-2?id=10246}
}

Your IPv4 address: 54.196.127.107
Switch to IPv6 connection

DNSSEC [dnssec]