SW.PCR

1// PTO-INSTRUCTION: {"assembly":["sw.pcr SrcL, [symbol]"],"block":[],"catalog_indices":[444],"catalog_records":[{"agu":{"action":"Store","address_kind":"PCRelative","offset_scale":2,"prefetch_returns_address":false,"signed_load":false,"size_bytes":4,"update_mode":"None"},"asm":"sw.pcr SrcL, [symbol]","constraints":[],"encoding":[{"index":0,"mask":"0x0000707f","match":"0x00002069","width_bits":32}],"encoding_kind":"L32","fields":[{"name":"SrcL","pieces":[{"instruction_lsb":15,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"simm","pieces":[{"instruction_lsb":20,"value_lsb":0,"width":12},{"instruction_lsb":7,"value_lsb":12,"width":5}],"signedness":"signed","width":17}],"form_id":"sw_pcr_32_436677679523","length_bits":32,"mnemonic":"SW.PCR","semantic_family":"AGU","semantic_group":"STA","semantic_handler":"ExecuteScalarStore","semantic_summary":"SW.PCR snapshots its scalar sources, forms its encoded address, and stores one aligned little-endian 4-byte value.","status":"accepted"}],"classification":["agu"],"contract":{"block_composition":["none"],"canonical_assembly":["sw.pcr SrcL, [symbol]"],"defaults":["Every displayed operand field is encoded explicitly; encoded zero is a value and never denotes omission."],"encoding_class":"standalone-encoded","examples":["sw.pcr SrcL, [symbol]"],"exceptions":["A fixed-bit mismatch, reserved field value, or unavailable selected T/U source raises Fault_IllegalInstruction before instruction effects.","A misaligned 4-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.","simm":"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.","simm assigns every signed 17-bit value -65536..65535; the encoded byte displacement is that value multiplied by 4.","Each memory address must be aligned to the 4-byte access size; a 4-byte access is the complete transfer unit."],"memory_effects":["After complete preflight, perform one little-endian 4-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":"simm","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 4-byte memory operation, publish any result or writeback, and then advance TPC."],"standalone_opcode":true,"state_effects":["Clear TPC bits 1:0, sign-extend the encoded displacement, multiply it by four, and add it modulo 2^PTO_XLEN.","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-SW-PCR","mnemonic":"SW.PCR","summary":"SW.PCR snapshots its scalar sources, forms its encoded address, and stores one aligned little-endian 4-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-SW-PCR-ADR-CONTRACT-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// Decisions: ADR-0024, ADR-0029.6// SW.PCR 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-SW-PCR-ADR-CONTRACT-00110// DOC-BEGIN: decode11readonly func InstructionContractOperation_SW_PCR() => ScalarOperation12begin13    return ScalarOperation_SW_PCR;14end;15// DOC-END: decode16// DOC-BEGIN: operation17readonly func InstructionContractHandler_SW_PCR()18    => ScalarSemanticHandler19begin20    return ScalarHandler_ExecuteScalarStore;21end;22
23pure func InstructionContractAGUAction_SW_PCR()24    => ScalarAGUAction25begin26    return ScalarAGU_Store;27end;28
29pure func InstructionContractAGUAddressKind_SW_PCR()30    => ScalarAGUAddressKind31begin32    return ScalarAGU_PCRelative;33end;34
35pure func InstructionContractAGUSizeBytes_SW_PCR()36    => integer {1,2,4,8}37begin38    return 4;39end;40
41pure func InstructionContractAGUOffsetScale_SW_PCR()42    => integer {0..3}43begin44    return 2;45end;46
47pure func InstructionContractAGUUpdateMode_SW_PCR()48    => AddressUpdateMode49begin50    return AddressUpdate_None;51end;52
53pure func InstructionContractAGUSignedLoad_SW_PCR()54    => boolean55begin56    return FALSE;57end;58
59pure func InstructionContractAGUPrefetchReturnsAddress_SW_PCR()60    => boolean61begin62    return FALSE;63end;64// DOC-END: operation65