SDI

1// PTO-INSTRUCTION: {"assembly":["sdi SrcL, [SrcR, simm]"],"block":[],"catalog_indices":[396],"catalog_records":[{"agu":{"action":"Store","address_kind":"Immediate","offset_scale":3,"prefetch_returns_address":false,"signed_load":false,"size_bytes":8,"update_mode":"None"},"asm":"sdi SrcL, [SrcR, simm]","constraints":[],"encoding":[{"index":0,"mask":"0x0000707f","match":"0x00003059","width_bits":32}],"encoding_kind":"L32","fields":[{"name":"SrcL","pieces":[{"instruction_lsb":15,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcR","pieces":[{"instruction_lsb":20,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"simm12","pieces":[{"instruction_lsb":25,"value_lsb":0,"width":7},{"instruction_lsb":7,"value_lsb":7,"width":5}],"signedness":"signed","width":12}],"form_id":"sdi_32_fab563230a66","length_bits":32,"mnemonic":"SDI","semantic_family":"AGU","semantic_group":"STA/BASE_IMM","semantic_handler":"ExecuteScalarStore","semantic_summary":"SDI snapshots its scalar sources, forms its encoded address, and stores one aligned little-endian 8-byte value.","status":"accepted"}],"classification":["agu"],"contract":{"block_composition":["none"],"canonical_assembly":["sdi SrcL, [SrcR, simm]"],"defaults":["Every displayed operand field is encoded explicitly; encoded zero is a value and never denotes omission."],"encoding_class":"standalone-encoded","examples":["sdi SrcL, [SrcR, simm]"],"exceptions":["A fixed-bit mismatch, reserved field value, or unavailable selected T/U source raises Fault_IllegalInstruction before instruction effects.","A misaligned 8-byte address raises Fault_DataAlignment before translation or permission. A later permission or bounded-memory failure raises Fault_DataPage at the original address.","A fault emits no successful memory event, performs no partial memory or destination effect, preserves pending writeback, and leaves TPC at the faulting instruction.","Recovery performs a full reissue: every address, source snapshot, preflight, memory operation, and destination is recomputed with no retained progress."],"field_contracts":{},"field_zero_meanings":{"SrcL":"Encoded zero reads the architectural zero GPR.","SrcR":"Encoded zero reads the architectural zero GPR.","simm12":"Encoded zero supplies a zero displacement; it does not denote omission."},"legality":["Every encoded Reg5 source uses the complete domain: codes 0..23 select absolute GPRs, codes 24..27 select T#1..T#4, and codes 28..31 select U#1..U#4 without consumption.","simm12 assigns every signed 12-bit value -2048..2047; the encoded byte displacement is that value multiplied by 8.","Each memory address must be aligned to the 8-byte access size; a 8-byte access is the complete transfer unit."],"memory_effects":["After complete preflight, perform one little-endian 8-byte store and record one relaxed store event.","A successful overlapping store invalidates the overlapping reservation; a nonoverlapping reservation remains valid."],"operands":[{"field":"SrcL","role":"Reg5 store-data source"},{"field":"SrcR","role":"Reg5 address-base source"},{"field":"simm12","role":"signed address displacement"}],"ordering":["Snapshot all explicit and implicit scalar sources before destination or memory effects; duplicate and source/destination aliases observe pre-instruction values.","Complete the relaxed 8-byte memory operation, publish any result or writeback, and then advance TPC."],"standalone_opcode":true,"state_effects":["Sign-extend simm12, multiply it by 8, and add it modulo 2^PTO_XLEN to the SrcR base.","Snapshot every store-data source before any memory effect or destination publication.","Successful execution advances TPC by 4 bytes; a rejected or faulting attempt does not retire."]},"depends_on":["PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"],"id":"PTO-SCALAR-SDI","mnemonic":"SDI","summary":"SDI snapshots its scalar sources, forms its encoded address, and stores one aligned little-endian 8-byte value.","surface":"scalar"}2// PTO-REVIEW: {"review_method":"formal-definition-read","outcome":"FORMAL-COMPLETE","reviewed_fields":["assembly","encoding","defaults","operation","state","memory","ordering","faults","reserved"]}3// NDF-BEGIN: PTO-SDI-ADR-CONTRACT-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// Decisions: ADR-0024, ADR-0029.6// SDI MUST snapshot scalar address/data sources, apply its mnemonic7// width and address-update mode, preflight access before effects, then commit8// the store event and any base update at the defined restart boundary.9// NDF-END: PTO-SDI-ADR-CONTRACT-00110// DOC-BEGIN: decode11readonly func InstructionContractOperation_SDI() => ScalarOperation12begin13    return ScalarOperation_SDI;14end;15// DOC-END: decode16// DOC-BEGIN: operation17readonly func InstructionContractHandler_SDI()18    => ScalarSemanticHandler19begin20    return ScalarHandler_ExecuteScalarStore;21end;22
23pure func InstructionContractAGUAction_SDI()24    => ScalarAGUAction25begin26    return ScalarAGU_Store;27end;28
29pure func InstructionContractAGUAddressKind_SDI()30    => ScalarAGUAddressKind31begin32    return ScalarAGU_Immediate;33end;34
35pure func InstructionContractAGUSizeBytes_SDI()36    => integer {1,2,4,8}37begin38    return 8;39end;40
41pure func InstructionContractAGUOffsetScale_SDI()42    => integer {0..3}43begin44    return 3;45end;46
47pure func InstructionContractAGUUpdateMode_SDI()48    => AddressUpdateMode49begin50    return AddressUpdate_None;51end;52
53pure func InstructionContractAGUSignedLoad_SDI()54    => boolean55begin56    return FALSE;57end;58
59pure func InstructionContractAGUPrefetchReturnsAddress_SDI()60    => boolean61begin62    return FALSE;63end;64// DOC-END: operation65