Formal Design and Verification of an Asynchronous SRAM Controller

Khomenko, V; Mokhov, A; Sokolov, D; Yakovlev, A

doi:10.1109/ACSD.2017.12

Formal Design and Verification of an Asynchronous SRAM Controller

Lookup NU author(s): Dr Victor Khomenko, Dr Andrey Mokhov, Dr Danil Sokolov, Professor Alex Yakovlev

Downloads

Accepted version [.pdf]

Licence

This is the authors' accepted manuscript of a conference proceedings (inc. abstract) that has been published in its final definitive form by IEEE Computing Society, 2017.

For re-use rights please refer to the publisher's terms and conditions.

Abstract

We propose a new design of an asynchronous speed-independent SRAM controller that is tolerant to variations in supply voltage and can trade off performance for power consumption. It uses the standard 6T memory cells and is more robust than a comparable speed-independent design in literature due to a delay-insensitive interface to bit-lines. Designing an asynchronous SRAM controller presents a fascinating challenge for the application of formal models: As there is no global clocking, the switching events are inherently partially ordered, with concurrency, sequencing and choice being inextricably intertwined. In contrast to previous designs, the proposed controller was systematically developed, synthesised, and formally verified.