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]