ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification

Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Rose Martonosi, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Modern Systems-on-Chip (SoCs) integrate heterogeneous compute elements ranging from non-programmable specialized accelerators to programmable CPUs and GPUs. To ensure correct system behavior, SoC verification techniques must account for inter-component interactions through shared memory, which necessitates reasoning about memory consistency models (MCMs) This paper presents ILA-MCM, a symbolic reasoning framework for automated SoC verification, where MCMs are integrated with Instruction-Level Abstractions (ILAs) that have been recently proposed to model architecture-level program-visible states and state updates in heterogeneous SoC components.ILA-MCM enables reasoning about system-wide properties that depend on functional state updates as well as ordering relations between them. Central to our approach is a novel facet abstraction, where a single program-visible variable is associated with potentially multiple facets that act as auxiliary state variables. Facets are updated by ILA »instructions,» and the required orderings between these updates are captured by MCM axioms. Thus, facets provide a symbolic constraint-based integration between operational ILA models and axiomatic MCM specifications. We have implemented a prototype ILA-MCM framework and use it to demonstrate two verification applications in this paper: (a) finding a known bug in an accelerator-based SoC, plus a new potential bug under a weaker MCM, and (b) checking that a recently proposed low-level GPU hardware implementation is correct with respect to a high-level ILA-MCM specification.

Original languageEnglish (US)
Title of host publicationProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
EditorsNikolaj Bjorner, Arie Gurfinkel
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages12-21
Number of pages10
ISBN (Electronic)9780983567882
DOIs
StatePublished - Jan 4 2019
Event18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018 - Austin, United States
Duration: Oct 30 2018Nov 2 2018

Publication series

NameProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018

Conference

Conference18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
CountryUnited States
CityAustin
Period10/30/1811/2/18

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design
  • Software

Fingerprint Dive into the research topics of 'ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification'. Together they form a unique fingerprint.

Cite this