PTO-SCALAR-MODEL-AGU-MEMORY

1// PTO-UNIT: {"id":"PTO-SCALAR-MODEL-AGU-MEMORY","surface":"scalar","classification":["model","agu","memory"],"depends_on":["PTO-SCALAR-MODEL-BRU-SEMANTICS","PTO-ARCH-MEMORY-MODEL-ORDERING"]}2// PTO-REQ-MEMORY-001, PTO-REQ-MEMORY-COMPLETION-001,3// PTO-REQ-MEMORY-TSO-001: profile-backed, little-endian memory with precise4// instruction-wide completion and PTO-TSO event extraction.5
6readonly func RangesOverlap(left_address: Word, left_size: integer,7                            right_address: Word, right_size: integer) => boolean8begin9    let left_start = UInt(left_address);10    let right_start = UInt(right_address);11    return left_start < right_start + right_size &&12           right_start < left_start + left_size;13end;14
15readonly func ReservationGranuleAddress() => Word16begin17    return _ReservationAddress - NaturalToWord(18        (UInt(_ReservationAddress) MOD PTO_RESERVATION_GRANULE_BYTES) as19            integer {0..262144});20end;21
22readonly impdef func TranslateDataAddress(address: Word,23                                          size_bytes: integer {1..262144},24                                          write: boolean) => Word25begin26    // The portable model uses identity translation.27    return address;28end;29
30readonly impdef func DataAccessPermitted(address: Word,31                                         size_bytes: integer {1..262144},32                                         write: boolean) => boolean33begin34    // The portable model exposes one bounded, readable, writable address space.35    return UInt(address) + size_bytes <= PTO_MODEL_MEMORY_BYTES;36end;37
38func ProbeDataAccess(address: Word,39                     size_bytes: integer {1..262144},40                     alignment_bytes: integer {1,2,4,8},41                     write: boolean) => DataAccessProbe42begin43    if UInt(address) MOD alignment_bytes != 0 then44        return DataAccessProbe {45            fault = Fault_DataAlignment,46            translated_address = address47        };48    end;49    let translated_address = TranslateDataAddress(address, size_bytes, write);50    if !DataAccessPermitted(translated_address, size_bytes, write) ||51       UInt(translated_address) + size_bytes > PTO_MODEL_MEMORY_BYTES then52        return DataAccessProbe {53            fault = Fault_DataPage,54            translated_address = translated_address55        };56    end;57    return DataAccessProbe {58        fault = Fault_None,59        translated_address = translated_address60    };61end;62
63func RaiseDataAccessFault(probe: DataAccessProbe, address: Word) => boolean64begin65    if probe.fault == Fault_None then return FALSE; end;66    SetFault(probe.fault, address);67    return TRUE;68end;69
70readonly func LoadTranslatedUnsigned(translated_address: Word,71                                     size_bytes: integer {1,2,4,8}) => Word72begin73    var result: Word = Zeros{PTO_XLEN};74    for byte_index = 0 to size_bytes - 1 do75        let byte_address = translated_address +76            NaturalToWord(byte_index as integer {0..262144});77        result[(byte_index * 8) +: 8] = ReadMemoryByte(byte_address);78    end;79    return result;80end;81
82readonly func LoadTranslatedBytes64(translated_address: Word) => array [[64]] of Byte83begin84    var result: array [[64]] of Byte;85    for byte_index = 0 to 63 do86        let byte_address = translated_address +87            NaturalToWord(byte_index as integer {0..262144});88        result[[byte_index]] = ReadMemoryByte(byte_address);89    end;90    return result;91end;92
93pure func Bytes64ChunkValue(value: array [[64]] of Byte,94                            chunk: integer {0..7}) => Word95begin96    var result: Word = Zeros{PTO_XLEN};97    for byte_index = 0 to 7 do98        let snapshot_index = (chunk * 8 + byte_index) as integer {0..63};99        result[(byte_index * 8) +: 8] = value[[snapshot_index]];100    end;101    return result;102end;103
104readonly func LoadTranslatedBytesBounded(translated_address: Word,105                                         byte_count: integer {0..63})106                                         => array [[64]] of Byte107begin108    var result: array [[64]] of Byte;109    for byte_index = 0 to 63 do110        if byte_index < byte_count then111            let byte_address = translated_address +112                NaturalToWord(byte_index as integer {0..262144});113            result[[byte_index]] = ReadMemoryByte(byte_address);114        else115            result[[byte_index]] = Zeros{8};116        end;117    end;118    return result;119end;120
121pure func NormalizeLoadedValue(value: Word,122                               size_bytes: integer {1,2,4,8},123                               signed_load: boolean) => Word124begin125    if !signed_load then return value; end;126    case size_bytes of127        when 1 => return SignExtend{PTO_XLEN}(value[7:0]);128        when 2 => return SignExtend{PTO_XLEN}(value[15:0]);129        when 4 => return SignExtend{PTO_XLEN}(value[31:0]);130        when 8 => return value;131    end;132end;133
134pure func NormalizeMemoryAccessValue(value: Word,135                                     size_bytes: integer {1,2,4,8}) => Word136begin137    case size_bytes of138        when 1 => return ZeroExtend{PTO_XLEN}(value[7:0]);139        when 2 => return ZeroExtend{PTO_XLEN}(value[15:0]);140        when 4 => return ZeroExtend{PTO_XLEN}(value[31:0]);141        when 8 => return value;142    end;143end;144
145func StoreTranslatedBytes64(original_address: Word, translated_address: Word,146                            value: array [[64]] of Byte)147begin148    for byte_index = 0 to 63 do149        let byte_address = translated_address +150            NaturalToWord(byte_index as integer {0..262144});151        WriteMemoryByte(byte_address, value[[byte_index]]);152    end;153    if _ReservationValid &&154       RangesOverlap(original_address, 64,155                     ReservationGranuleAddress(),156                     PTO_RESERVATION_GRANULE_BYTES) then157        _ReservationValid = FALSE;158    end;159end;160
161func StoreTranslatedBytesBounded(original_address: Word,162                                 translated_address: Word,163                                 byte_count: integer {0..63},164                                 value: array [[64]] of Byte)165begin166    for byte_index = 0 to 63 do167        if byte_index < byte_count then168            let byte_address = translated_address +169                NaturalToWord(byte_index as integer {0..262144});170            WriteMemoryByte(byte_address, value[[byte_index]]);171        end;172    end;173    if _ReservationValid &&174       RangesOverlap(original_address, byte_count,175                     ReservationGranuleAddress(),176                     PTO_RESERVATION_GRANULE_BYTES) then177        _ReservationValid = FALSE;178    end;179end;180
181func StoreTranslatedFillBounded(original_address: Word,182                                translated_address: Word,183                                byte_count: integer {0..63},184                                value: Byte)185begin186    for byte_index = 0 to 63 do187        if byte_index < byte_count then188            let byte_address = translated_address +189                NaturalToWord(byte_index as integer {0..262144});190            WriteMemoryByte(byte_address, value);191        end;192    end;193    if _ReservationValid &&194       RangesOverlap(original_address, byte_count,195                     ReservationGranuleAddress(),196                     PTO_RESERVATION_GRANULE_BYTES) then197        _ReservationValid = FALSE;198    end;199end;200
201func StoreTranslated(original_address: Word, translated_address: Word,202                     size_bytes: integer {1,2,4,8}, value: Word)203begin204    for byte_index = 0 to size_bytes - 1 do205        let byte_address = translated_address +206            NaturalToWord(byte_index as integer {0..262144});207        WriteMemoryByte(byte_address, value[(byte_index * 8) +: 8]);208    end;209    if _ReservationValid &&210       RangesOverlap(original_address, size_bytes,211                     ReservationGranuleAddress(),212                     PTO_RESERVATION_GRANULE_BYTES) then213        _ReservationValid = FALSE;214    end;215end;216
217func LoadWithOrder(address: Word, size_bytes: integer {1,2,4,8},218                   order: MemoryOrder) => Word219begin220    let probe = ProbeDataAccess(address, size_bytes, size_bytes, FALSE);221    if RaiseDataAccessFault(probe, address) then return Zeros{PTO_XLEN}; end;222    let value = LoadTranslatedUnsigned(probe.translated_address, size_bytes);223    RecordLoadEvent(probe.translated_address, size_bytes, value, order);224    return value;225end;226
227func LoadUnsigned(address: Word, size_bytes: integer {1,2,4,8}) => Word228begin229    return LoadWithOrder(address, size_bytes, MemoryOrder_Relaxed);230end;231
232func LoadSigned(address: Word, size_bytes: integer {1,2,4,8}) => Word233begin234    let value = LoadUnsigned(address, size_bytes);235    return NormalizeLoadedValue(value, size_bytes, TRUE);236end;237
238func StoreWithOrder(address: Word, size_bytes: integer {1,2,4,8}, value: Word,239                    order: MemoryOrder)240begin241    let probe = ProbeDataAccess(address, size_bytes, size_bytes, TRUE);242    if RaiseDataAccessFault(probe, address) then return; end;243    StoreTranslated(address, probe.translated_address, size_bytes, value);244    RecordStoreEvent(probe.translated_address, size_bytes, value, order);245end;246
247func Store(address: Word, size_bytes: integer {1,2,4,8}, value: Word)248begin249    StoreWithOrder(address, size_bytes, value, MemoryOrder_Relaxed);250end;251