PTO-ARCH-MEMORY-MODEL-MEMORY-EVENTS

1// PTO-UNIT: {"id":"PTO-ARCH-MEMORY-MODEL-MEMORY-EVENTS","surface":"arch","classification":["memory-model","memory-events"],"depends_on":["PTO-ARCH-MEMORY-MODEL-ADDRESS-SPACE"]}2// PTO-REQ-MEMORY-TSO-001: bounded executable candidate-execution checker for3// PTO total store order. The event bound is verification infrastructure, not4// an architectural limit on agents or executions.5
6pure func MemoryEventIsRead(event: MemoryEvent) => boolean7begin8    return event.kind == MemoryEvent_Load || event.kind == MemoryEvent_Atomic;9end;10
11pure func MemoryEventIsWrite(event: MemoryEvent) => boolean12begin13    return event.kind == MemoryEvent_InitialWrite ||14           event.kind == MemoryEvent_Store ||15           (event.kind == MemoryEvent_Atomic && event.write_performed);16end;17
18pure func MemoryEventIsAccess(event: MemoryEvent) => boolean19begin20    return MemoryEventIsRead(event) || MemoryEventIsWrite(event);21end;22
23pure func MemoryEventsShareLocation(left: MemoryEvent,24                                    right: MemoryEvent) => boolean25begin26    return left.address == right.address && left.size_bytes == right.size_bytes;27end;28
29pure func MemoryEventClass(event: MemoryEvent) => bits(4)30begin31    // FENCE.D mask bits are: data read, data write, device, and instruction.32    // The current candidate model contains data events; atomic events are both33    // reads and writes. Instruction and device classes remain explicit masks.34    case event.kind of35        when MemoryEvent_Load => return '0001';36        when MemoryEvent_Store, MemoryEvent_InitialWrite => return '0010';37        when MemoryEvent_Atomic => return '0011';38        when MemoryEvent_Fence => return Zeros{4};39    end;40end;41
42func ResetMemoryExecution()43begin44    _MemoryEventCount = 0;45end;46
47// Production event extraction is an explicit verification mode because the48// bounded event array is model-checking infrastructure, not an architectural49// execution limit. Manual candidate construction remains available while50// capture is disabled.51func StartMemoryEventCapture(agent: MemoryAgentId)52begin53    ResetMemoryExecution();54    _CurrentMemoryAgent = agent;55    _MemoryEventCaptureEnabled = TRUE;56end;57
58func SelectMemoryEventAgent(agent: MemoryAgentId)59begin60    _CurrentMemoryAgent = agent;61end;62
63func StopMemoryEventCapture()64begin65    _MemoryEventCaptureEnabled = FALSE;66end;67
68func AddMemoryEvent(event: MemoryEvent) => MemoryEventIndex69begin70    assert _MemoryEventCount < PTO_MODEL_MEMORY_EVENTS;71    let index = _MemoryEventCount as MemoryEventIndex;72    _MemoryEvents[[index]] = event;73    _MemoryEventCount = (_MemoryEventCount + 1) as74        integer {0..PTO_MODEL_MEMORY_EVENTS};75    return index;76end;77
78func AddInitialWriteEvent(address: Word, size_bytes: integer {1,2,4,8},79                          value: Word) => MemoryEventIndex80begin81    return AddMemoryEvent(MemoryEvent {82        kind = MemoryEvent_InitialWrite,83        agent = 0,84        address = address,85        size_bytes = size_bytes,86        read_value = Zeros{PTO_XLEN},87        write_value = NormalizeMemoryAccessValue(value, size_bytes),88        write_performed = TRUE,89        order = MemoryOrder_Relaxed,90        read_from = 0,91        coherence_rank = 0,92        fence_predecessor = Zeros{4},93        fence_successor = Zeros{4}94    });95end;96
97func AddLoadEvent(agent: MemoryAgentId, address: Word,98                  size_bytes: integer {1,2,4,8}, value: Word,99                  order: MemoryOrder) => MemoryEventIndex100begin101    return AddMemoryEvent(MemoryEvent {102        kind = MemoryEvent_Load,103        agent = agent,104        address = address,105        size_bytes = size_bytes,106        read_value = NormalizeMemoryAccessValue(value, size_bytes),107        write_value = Zeros{PTO_XLEN},108        write_performed = FALSE,109        order = order,110        read_from = 0,111        coherence_rank = 0,112        fence_predecessor = Zeros{4},113        fence_successor = Zeros{4}114    });115end;116
117func AddStoreEvent(agent: MemoryAgentId, address: Word,118                   size_bytes: integer {1,2,4,8}, value: Word,119                   order: MemoryOrder, rank: MemoryCoherenceRank)120                   => MemoryEventIndex121begin122    return AddMemoryEvent(MemoryEvent {123        kind = MemoryEvent_Store,124        agent = agent,125        address = address,126        size_bytes = size_bytes,127        read_value = Zeros{PTO_XLEN},128        write_value = NormalizeMemoryAccessValue(value, size_bytes),129        write_performed = TRUE,130        order = order,131        read_from = 0,132        coherence_rank = rank,133        fence_predecessor = Zeros{4},134        fence_successor = Zeros{4}135    });136end;137
138func AddAtomicEvent(agent: MemoryAgentId, address: Word,139                    size_bytes: integer {1,2,4,8}, read_value: Word,140                    write_value: Word, order: MemoryOrder,141                    rank: MemoryCoherenceRank) => MemoryEventIndex142begin143    return AddAtomicOutcomeEvent(agent, address, size_bytes, read_value,144        write_value, order, rank, TRUE);145end;146
147func AddAtomicOutcomeEvent(agent: MemoryAgentId, address: Word,148                           size_bytes: integer {1,2,4,8}, read_value: Word,149                           write_value: Word, order: MemoryOrder,150                           rank: MemoryCoherenceRank,151                           write_performed: boolean) => MemoryEventIndex152begin153    return AddMemoryEvent(MemoryEvent {154        kind = MemoryEvent_Atomic,155        agent = agent,156        address = address,157        size_bytes = size_bytes,158        read_value = NormalizeMemoryAccessValue(read_value, size_bytes),159        write_value = NormalizeMemoryAccessValue(write_value, size_bytes),160        write_performed = write_performed,161        order = order,162        read_from = 0,163        coherence_rank = rank,164        fence_predecessor = Zeros{4},165        fence_successor = Zeros{4}166    });167end;168
169func AddDataFenceEvent(agent: MemoryAgentId, predecessor: bits(4),170                       successor: bits(4)) => MemoryEventIndex171begin172    return AddMemoryEvent(MemoryEvent {173        kind = MemoryEvent_Fence,174        agent = agent,175        address = Zeros{PTO_XLEN},176        size_bytes = 1,177        read_value = Zeros{PTO_XLEN},178        write_value = Zeros{PTO_XLEN},179        write_performed = FALSE,180        order = MemoryOrder_AcquireRelease,181        read_from = 0,182        coherence_rank = 0,183        fence_predecessor = predecessor,184        fence_successor = successor185    });186end;187