uSpec

[Google Scholar]

Notes: weak memory
Papers: hsiao:micro:2021

Descriptions of memory consistency models as first order logic that emphasize the connection with pipeline stages in a processor. The approach is based on an axiomatic approach to defining happens before relations within instructions and between instructions.

  • Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations [hsiao:micro:2021]
  • RTLcheck: Verifying the Memory Consistency of RTL Designs [manerkar:micro:2017]
  • Axiomatic Hardware-Software Contracts for Security [mosier:isca:2022]
  • Opening Pandora's Box: A Systematic Study of New Ways Microarchitecture Can Leak Private Data [vicarte:isca:2021]