Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations
Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline Trippel
Abstract
Modern hardware complexity makes it challenging to determine if a given microarchitecture adheres to a particular memory consistency model (MCM). This observation inspired the Check tools, which formally check that a specific microarchitecture correctly implements an MCM with respect to a suite of litmus test programs. Unfortunately, despite their effectiveness and efficiency, the Check tools must be supplied a microarchitecture in the guise of a manually constructed axiomatic specification, called a μspec model.
Topics & Concepts
Computer scienceMicroarchitectureSuiteMemory modelProgramming languageImplementationConsistency (knowledge bases)Sequential consistencyComputer architectureLitmusConsistency modelParallel computingTest suiteEmbedded systemShared memoryArtificial intelligenceTest caseMachine learningCorrectnessHistoryArchaeologyChemistryPhysical chemistryRegression analysisParallel Computing and Optimization TechniquesEmbedded Systems Design TechniquesFormal Methods in Verification