Five EmbedDev logo Five EmbedDev

An Embedded RISC-V Blog
RISC-V Instruction Set Manual, Volume I: RISC-V User-Level ISA , isa-449cd0c 2023/04/18

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)