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]