SHI

1// PTO-INSTRUCTION: {"assembly":["shi SrcL, [SrcR, simm]"],"block":[],"catalog_indices":[419],"catalog_records":[{"agu":{"action":"Store","address_kind":"Immediate","offset_scale":1,"prefetch_returns_address":false,"signed_load":false,"size_bytes":2,"update_mode":"None"},"asm":"shi SrcL, [SrcR, simm]","constraints":[],"encoding":[{"index":0,"mask":"0x0000707f","match":"0x00001059","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":"shi_32_21351c202204","length_bits":32,"mnemonic":"SHI","semantic_family":"AGU","semantic_group":"STA/BASE_IMM","semantic_handler":"ExecuteScalarStore","semantic_summary":"SHI snapshots its scalar sources, forms its encoded address, and stores one aligned little-endian 2-byte value.","status":"accepted"}],"classification":["agu"],"contract":{"block_composition":["none"],"canonical_assembly":["shi 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":["shi 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 2-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 2.","Each memory address must be aligned to the 2-byte access size; a 2-byte access is the complete transfer unit."],"memory_effects":["After complete preflight, perform one little-endian 2-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 2-byte memory operation, publish any result or writeback, and then advance TPC."],"standalone_opcode":true,"state_effects":["Sign-extend simm12, multiply it by 2, 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-SHI","mnemonic":"SHI","summary":"SHI snapshots its scalar sources, forms its encoded address, and stores one aligned little-endian 2-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-SHI-ADR-CONTRACT-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// Decisions: ADR-0024, ADR-0029.6// SHI 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-SHI-ADR-CONTRACT-00110// DOC-BEGIN: decode11readonly func InstructionContractOperation_SHI() => ScalarOperation12begin13    return ScalarOperation_SHI;14end;15// DOC-END: decode16// DOC-BEGIN: operation17readonly func InstructionContractHandler_SHI()18    => ScalarSemanticHandler19begin20    return ScalarHandler_ExecuteScalarStore;21end;22
23pure func InstructionContractAGUAction_SHI()24    => ScalarAGUAction25begin26    return ScalarAGU_Store;27end;28
29pure func InstructionContractAGUAddressKind_SHI()30    => ScalarAGUAddressKind31begin32    return ScalarAGU_Immediate;33end;34
35pure func InstructionContractAGUSizeBytes_SHI()36    => integer {1,2,4,8}37begin38    return 2;39end;40
41pure func InstructionContractAGUOffsetScale_SHI()42    => integer {0..3}43begin44    return 1;45end;46
47pure func InstructionContractAGUUpdateMode_SHI()48    => AddressUpdateMode49begin50    return AddressUpdate_None;51end;52
53pure func InstructionContractAGUSignedLoad_SHI()54    => boolean55begin56    return FALSE;57end;58
59pure func InstructionContractAGUPrefetchReturnsAddress_SHI()60    => boolean61begin62    return FALSE;63end;64// DOC-END: operation65