Memory Model

Concept

A memory model defines how memory operations behave. In formal language and architecture work it can specify the semantics of loads, stores, permissions, and reordering; in CPU verification testbenches it can also mean the simulated memory component that stores programs and serves instruction and data requests.

First seen 5/27/2026

Last seen 5/28/2026

Evidence 3 chunks

Wiki v1

WIKI

Overview

A memory model describes the behavior of operations on memory. In formal programming-language semantics, it is the core component that defines how memory operations behave. In weak-memory architecture research, a memory model captures which load and store orderings are allowed when processors and compilers preserve uniprocessor optimizations in shared-memory multiprocessors.

The term is also used in hardware verification to mean a simulated memory component in a testbench. In that setting, the memory model is not necessarily a formal consistency model; it is a testbench resource that stores program images, responds to memory transactions, and may expose memory-mapped test peripherals.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

Ibex Core ← uses 95% 1e

Ibex testbench instantiates a memory model for instruction and data memory.

LINKED ENTITIES

1 links

Ibex Core USES Extracted graph relationship

CITATIONS

10 sources

10 citations — click to expand

[1] A memory model is the core of a formal semantics for an imperative programming language and describes the behavior of operations on memory. A Formal C Memory Model for Separation Logic

[2] The cited C11 formal memory model addresses both typed high-level accesses and low-level bit manipulation, incorporates C11 restrictions, includes a rich permission model, and was formalized in Coq. A Formal C Memory Model for Separation Logic

[3] Weak memory models are motivated by preserving uniprocessor optimizations in shared-memory multiprocessors, and the cited GAM model allows all four load/store reorderings. Constructing a Weak Memory Model

[4] In the Ibex testbench, a single memory model is loaded with the compiled assembly test program at the beginning of each test and acts as a unified instruction/data memory for both memory interface agents. [PDF] UVM based design veri cation of a RISC-V CPU core - POLITesi

[5] The Ibex testbench has separate memory interface agents for instruction fetch and the LSU interface, and their slave sequences wait for core memory requests and grant instruction or data requests. [PDF] UVM based design veri cation of a RISC-V CPU core - POLITesi

[6] Ibex tests coordinate loading the compiled assembly binary into the testbench memory model, checking core status, and handling test timeouts. [PDF] UVM based design veri cation of a RISC-V CPU core - POLITesi

[7] The Ibex co-simulation setup checks executed instructions and memory transactions against an ISS and uses RVFI to provide information about retired instructions and synchronous traps. [PDF] UVM based design veri cation of a RISC-V CPU core - POLITesi

[8] In the CORE-V UVM environment, programs can access the full address range supported by the testbench memory model plus memory-mapped virtual peripherals. [PDF] UVM based design veri cation of a RISC-V CPU core - POLITesi

[9] The CORE-V testbench memory module implements virtual peripherals by responding to read or write cycles at specific addresses on the data bus. [PDF] UVM based design veri cation of a RISC-V CPU core - POLITesi

[10] CORE-V Board Support Package files align test-program resources with DUT and testbench resources, including linker scripts, memory regions, CSR configuration files, and startup assembly. [PDF] UVM based design veri cation of a RISC-V CPU core - POLITesi