Detail výsledku

An Abstraction of Multi-Port Memories with Arbitrary Addressable Units

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. Computer Aided Systems Theory - EUROCAST 2013. Lecture Notes in Computer Science. Berlin Heidelberg: Springer Verlag, 2013. p. 460-468. ISBN: 978-3-642-53855-1.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Charvát Lukáš, Ing., Ph.D., UITS (FIT)
Smrčka Aleš, Ing., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
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

Rok
2013
Strany
460–468
Sborník
Computer Aided Systems Theory - EUROCAST 2013
Řada
Lecture Notes in Computer Science
Svazek
8111
Konference
Fourteenth International Conference On Computer Aided Systems Theory
ISBN
978-3-642-53855-1
Vydavatel
Springer Verlag
Místo
Berlin Heidelberg
BibTeX 
@inproceedings{BUT103508,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="An Abstraction of Multi-Port Memories with Arbitrary Addressable Units",
  booktitle="Computer Aided Systems Theory - EUROCAST 2013",
  year="2013",
  series="Lecture Notes in Computer Science",
  volume="8111",
  pages="460--468",
  publisher="Springer Verlag",
  address="Berlin Heidelberg",
  isbn="978-3-642-53855-1"
}
Projekty
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Pokročilé bezpečné, spolehlivé a adaptivní IT, VUT, Vnitřní projekty VUT, FIT-S-11-1, zahájení: 2011-01-01, ukončení: 2013-12-31, ukončen
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Systém pro programování a realizaci vestavěných systémů, MPO, TIP, FR-TI1/038, zahájení: 2009-07-01, ukončení: 2013-06-30, ukončen
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru