Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
CHARVÁT, L. SMRČKA, A. VOJNAR, T.
Originální název
An Abstraction of Multi-Port Memories with Arbitrary Addressable Units
Typ
článek ve sborníku mimo WoS a Scopus
Jazyk
angličtina
Originální 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 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.
Klíčová slova
memory, register file, automatic formal verification, model checking
Autoři
CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.
Rok RIV
2013
Vydáno
15. 2. 2013
Nakladatel
The Universidad de Las Palmas de Gran Canaria
Místo
Las Palmas de Grand Canaria
ISBN
978-84-695-6971-9
Kniha
Proceedings of the 14th Computer Aided Systems Theory
Strany od
254
Strany do
255
Strany počet
2
URL
https://www.fit.vut.cz/research/publication/10246/
BibTex
@inproceedings{BUT103450, author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}", title="An Abstraction of Multi-Port Memories with Arbitrary Addressable Units", booktitle="Proceedings of the 14th Computer Aided Systems Theory", year="2013", pages="254--255", publisher="The Universidad de Las Palmas de Gran Canaria", address="Las Palmas de Grand Canaria", isbn="978-84-695-6971-9", url="https://www.fit.vut.cz/research/publication/10246/" }