Five EmbedDev

An Embedded RISC-V Blog

Preface

1. Introduction

2. RV32I Base Integer Instruction Set, Version 2.1

3. Zifencei Instruction-Fetch Fence, Version 2.0

4. Zihintpause Pause Hint, Version 2.0

5. RV32E Base Integer Instruction Set, Version 1.9

6. RV64I Base Integer Instruction Set, Version 2.1

7. RV128I Base Integer Instruction Set, Version 1.7

8. M Standard Extension for Integer Multiplication and

9. A Standard Extension for Atomic Instructions, Version 2.1

10. Zicsr, Control and Status Register (CSR) Instructions, Version 2.0

11. Counters

12. F Standard Extension for Single-Precision Floating-Point,

13. D Standard Extension for Double-Precision Floating-Point,

14. Q Standard Extension for Quad-Precision Floating-Point,

15. Zfh and Zfhmin Standard Extensions for Half-Precision Floating-Point,

16. RVWMO Memory Consistency Model, Version 2.0

17. C Standard Extension for Compressed Instructions, Version

18. B Standard Extension for Bit Manipulation, Version 0.0

19. J Standard Extension for Dynamically Translated Languages, Version 0.0

20. P Standard Extension for Packed-SIMD Instructions,

21. V Standard Extension for Vector Operations, Version 0.7

22. Zam Standard Extension for Misaligned Atomics, v0.1

23. Zfinx, Zdinx, Zhinx, Zhinxmin: Standard Extensions for Floating-Point in Integer Registers, Version 1.0.0-rc

24. Ztso Standard Extension for Total Store Ordering, v0.1

25. RV32/64G Instruction Set Listings

26. Extending RISC-V

27. ISA Extension Naming Conventions

28. History and Acknowledgments

CSR Dependency Tracking Granularity

Source and Destination Register Listings

RVWMO Explanatory Material, Version 0.1

Formal Memory Model Specifications, Version 0.1

Formal Axiomatic Specification in Alloy

Formal Axiomatic Specification in Herd

An Operational Memory Model

RISC-V Instruction Set Manual, Volume I: RISC-V User-Level ISA , Priv-v1.12 2021/12/03

Formal Axiomatic Specification in Alloy

We present a formal specification of the RVWMO memory model in Alloy (http://alloy.mit.edu). This model is available online at https://github.com/daniellustig/riscv-memory-model.

The online material also contains some litmus tests and some examples of how Alloy can be used to model check some of the mappings in Section [sec:memory:porting].

The RVWMO memory model formalized in Alloy (1/5: PPO)

The RVWMO memory model formalized in Alloy (2/5: Axioms)

The RVWMO memory model formalized in Alloy (3/5: model of memory)

The RVWMO memory model formalized in Alloy (4/5: Basic model rules)

The RVWMO memory model formalized in Alloy (5/5: Auxiliaries)

© RISC-V Foundation, CC BY 4.0. Coverted to HTML from src/memory-model-alloy.tex(Priv-v1.12) using Pandoc. For the official specifications refer to riscv.org.