The Memory Marionette Model (m3) is a powerful verification library designed to expose subtle bugs in multicore memory subsystems. By implementing the Marionette Model methodology, m3 brings unmatched precision to memory operation tracking and validation—making it an essential tool for anyone serious about building reliable multicore processors.
- Enable co-simulation of multicore systems running share memory programs
- Verify correct memory behavior in multicore systems
- Track and validate memory operation ordering
- Ensure memory consistency across cores
- Support both in-order and out-of-order execution models
- Provide comprehensive debugging and error detection capabilities
-
Marionette Model: Unlike traditional single-point "at commit" verification, m3 uses a marionette model that tracks operations throughout execution, enabling true co-simulation of multicore shared memory programs
-
Comprehensive Operation Tracking: Tracks loads, stores, and atomic operations from issue through completion, with support for store-to-load forwarding and store merging
-
Verification Mechanisms: Memory consistency checking, operation ordering validation, error detection and reporting, comprehensive state tracking
-
Flexible Integration: Support for multiple emulators (Dromajo, Spike), bridge-based architecture for easy extension, configurable verification parameters
-
Clone the repository:
git clone https://github.com/texerai/m3.git cd m3 -
Install dependencies:
# Ubuntu/Debian sudo apt install build-essential cmake # macOS brew install cmake
-
Build the project:
mkdir build cd build cmake .. make -j
The library will be built as libm3.a in the build directory. Headers will be in include/.
