TY - GEN
T1 - ILA-MCM
T2 - 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
AU - Zhang, Hongce
AU - Trippel, Caroline
AU - Manerkar, Yatin A.
AU - Gupta, Aarti
AU - Martonosi, Margaret Rose
AU - Malik, Sharad
N1 - Publisher Copyright:
© 2018 FMCAD Inc.
PY - 2018/7/2
Y1 - 2018/7/2
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85061629707&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85061629707&partnerID=8YFLogxK
U2 - 10.23919/FMCAD.2018.8603015
DO - 10.23919/FMCAD.2018.8603015
M3 - Conference contribution
AN - SCOPUS:85061629707
T3 - Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
SP - 12
EP - 21
BT - Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
A2 - Bjorner, Nikolaj
A2 - Gurfinkel, Arie
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 30 October 2018 through 2 November 2018
ER -