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.
Papers related to uSpec
- 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]