Repository logo
 

A consistency checker for memory subsystem traces

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Naylor, M 
Moore, SW 
Mujumdar, A 

Abstract

Verifying the memory subsystem in a modern shared-memory multiprocessor is a big challenge. Optimized implementations are highly sophisticated, yet must provide subtle consistency and liveness guarantees for the correct execution of concurrent programs. We present a tool that supports efficient specification-based testing of the memory subsystem against a range of formally specified consistency models. Our tool operates directly on the memory subsystem interface, promoting a compositional approach to system-on-chip verification, and can be used to search for simple failure cases – assisting rapid debug. It has recently been incorporated into the development flows of two open-source implementations – Berkeley’s Rocket Chip (RISCV) and Cambridge’s BERI (MIPS) – where it has uncovered a number of serious bugs.

Description

Keywords

40 Engineering, 4008 Electrical Engineering, 4009 Electronics, Sensors and Digital Hardware

Journal Title

Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016

Conference Name

2016 Formal Methods in Computer-Aided Design (FMCAD)

Journal ISSN

Volume Title

Publisher

IEEE
Sponsorship
This work was supported by DARPA/AFRL contracts FA8750-10-C-0237 (CTSRD) and FA8750-11-C-0249 (MRC2), and EPSRC grant EP/K008528/1 (REMS).
Relationships
Is supplemented by: