		Search-engine friendly clone of the ACL2 documentation.

Riscv

Reads-over-writes

Read-over-write theorems.

We prove typical theorems that rewrite read operations on states applied to write operations on states. These are useful for validating the specification of the operations, as well as for reasoning.

Subtopics

Read-xreg-of-write-memory-theorems: Theorems about reads of registers over writes of memory.
Read-xreg-of-write-xreg-theorems: Theorems about reads of registers over writes of registers.
Read-memory-of-write-pc-theorems: Theorems about reads of memory over writes of program counter.
Read-xreg-of-write-pc-theorems: Theorems about reads of registers over writes of program counter.
Read-memory-of-write-xreg-theorems: Theorems about reads of memory over writes of registers.
Read-memory-of-write-memory-theorems: Theorems about reads of memory over writes of memory.
Read-pc-of-write-pc-theorems: Theorems about reads of program counter over writes of program counter.
Read-pc-of-write-memory-theorems: Theorems about reads of program counter over writes of memory.
Read-instruction-of-write-pc-theorems: Theorems about reads of instructions over writes of program counter.
Read-instruction-of-write-xreg-theorems: Theorems about reads of instructions over writes of registers.
Read-instruction-of-write-memory-theorems: Theorems about reads of instructions over writes of memory.
Read-pc-of-write-xreg-theorems: Theorems about reads of program counter over writes of registers.