Detail publikace

An Abstraction of Multi-Port Memories with Arbitrary Addressable Units

Originální název

An Abstraction of Multi-Port Memories with Arbitrary Addressable Units

Anglický název

An Abstraction of Multi-Port Memories with Arbitrary Addressable Units

Jazyk

en

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.

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

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",
  annote="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.",
  address="Springer Verlag",
  booktitle="Computer Aided Systems Theory - EUROCAST 2013",
  chapter="103508",
  edition="Lecture Notes in Computer Science",
  howpublished="online",
  institution="Springer Verlag",
  year="2013",
  month="may",
  pages="460--468",
  publisher="Springer Verlag",
  type="conference paper"
}