Publication Details

An Abstraction of Multi-Port Memories with Arbitrary Addressable Units

CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. In: Computer Aided Systems Theory - EUROCAST 2013. Lecture Notes in Computer Science, vol. 8111. Berlin Heidelberg: Springer Verlag, 2013, pp. 460-468. ISBN 978-3-642-53855-1.
Czech title
Abstrakce víceportových pamětí s libovolnými adresovanými jednotkami
Type
conference paper
Language
english
Authors
Keywords

memory, register file, automatic formal verification, model checking

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 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.

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 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.

Published
2013
Pages
460-468
Proceedings
Computer Aided Systems Theory - EUROCAST 2013
Series
Lecture Notes in Computer Science
Volume
8111
Conference
Fourteenth International Conference On Computer Aided Systems Theory, Las Palmas de Gran Canaria, ES
ISBN
978-3-642-53855-1
Publisher
Springer Verlag
Place
Berlin Heidelberg, DE
BibTeX
@INPROCEEDINGS{FITPUB10352,
   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 = "460--468",
   booktitle = "Computer Aided Systems Theory - EUROCAST 2013",
   series = "Lecture Notes in Computer Science",
   volume = 8111,
   year = 2013,
   location = "Berlin Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-53855-1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10352"
}
Back to top