Operands and parameters
RegDst- Reg5 destination or discard
SrcL- Reg5 value source
SrcR- Reg5 shift-count source
SRA performs a arithmetic right shift of the PTO_XLEN source by the low six bits of the snapshotted SrcR; the XLEN result is published directly.
PTO-SCALAR-SRAsra SrcL, SrcR, ->{t, u, Rd}| Field | Bits | Signedness | Architectural role | Encoded zero |
|---|---|---|---|---|
RegDst | 5 | encoding-defined | Reg5 destination or discard | Encoded zero discards the result. |
SrcL | 5 | encoding-defined | Reg5 value source | Encoded zero reads the architectural zero GPR. |
SrcR | 5 | encoding-defined | Reg5 shift-count source | Encoded zero reads zero and therefore selects shift amount zero. |
Loading WaveDrom diagram… The encoding table and WaveJSON remain available below.
| Decoded item | Bit range | Value |
|---|---|---|
| Constant | 31:25 | 7'b0000000 |
| SrcR | 24:20 | variable |
| SrcL | 19:15 | variable |
| Constant | 14:12 | 3'b110 |
| RegDst | 11:7 | variable |
| Constant | 6:0 | 7'b0000101 |
{
"reg": [
{
"bits": 7,
"name": "7'b0000101"
},
{
"bits": 5,
"name": "RegDst"
},
{
"bits": 3,
"name": "3'b110"
},
{
"bits": 5,
"name": "SrcL"
},
{
"bits": 5,
"name": "SrcR"
},
{
"bits": 7,
"name": "7'b0000000"
}
],
"config": {
"bits": 32,
"fontsize": 13,
"hspace": 900,
"lanes": 1,
"offset": 0
}
}sra SrcL, SrcR, ->{t, u, Rd}
RegDstSrcLSrcRThis Operation comes directly from the instruction owner; the page does not rewrite its behavior.
readonly func InstructionContractOperation_SRA() => ScalarOperationbegin return ScalarOperation_SRA;end;readonly func InstructionContractHandler_SRA() => ScalarSemanticHandlerbegin return ScalarHandler_ScalarBinary;end;
pure func InstructionContractShiftAmount_SRA(right: Word) => integer {0..63}begin return UInt(right[5:0]);end;
pure func InstructionContractResult_SRA(left: Word, right: Word) => Wordbegin let amount = InstructionContractShiftAmount_SRA(right); let shifted = ASR(left, amount); return shifted;end;
pure func InstructionContractIsWordOperation_SRA() => booleanbegin return FALSE;end;// PTO-INSTRUCTION: {"assembly":["sra SrcL, SrcR, ->{t, u, Rd}"],"block":[],"catalog_indices":[425],"catalog_records":[{"asm":"sra SrcL, SrcR, ->{t, u, Rd}","constraints":[],"encoding":[{"index":0,"mask":"0xfe00707f","match":"0x00006005","width_bits":32}],"encoding_kind":"L32","fields":[{"name":"RegDst","pieces":[{"instruction_lsb":7,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"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}],"form_id":"sra_32_ba03eea6386b","length_bits":32,"mnemonic":"SRA","semantic_family":"ALU","semantic_group":"ALU","semantic_handler":"ScalarBinary","semantic_summary":"SRA performs a arithmetic right shift of the PTO_XLEN source by the low six bits of the snapshotted SrcR; the XLEN result is published directly.","status":"accepted"}],"classification":["alu"],"contract":{"block_composition":["none"],"canonical_assembly":["sra SrcL, SrcR, ->{t, u, Rd}"],"defaults":["SrcL, SrcR, and RegDst are required fields; no field can be omitted.","The low six bits of the snapshotted SrcR select the shift amount 0 through 63; every higher SrcR bit is ignored for the amount."],"encoding_class":"standalone-encoded","examples":["sra a0, a1, ->a2","sra t#1, u#1, ->u","sra zero, zero, ->zero"],"exceptions":["SRA raises no arithmetic exception; shifted-out bits are discarded.","An unavailable T/U source raises Fault_IllegalInstruction before the destination effect and successful TPC advance."],"field_contracts":{},"field_zero_meanings":{"RegDst":"Encoded zero discards the result.","SrcL":"Encoded zero reads the architectural zero GPR.","SrcR":"Encoded zero reads zero and therefore selects shift amount zero."},"legality":["SrcL and SrcR codes 0..23 select absolute GPRs, 24..27 select T#1..T#4, and 28..31 select U#1..U#4 without consumption.","RegDst codes 0 and 24..29 discard, code 30 pushes U, code 31 pushes T, and codes 1..23 write GPRs.","All SrcR values are legal; only its low six bits contribute to the shift amount."],"memory_effects":["none"],"operands":[{"field":"RegDst","role":"Reg5 destination or discard"},{"field":"SrcL","role":"Reg5 value source"},{"field":"SrcR","role":"Reg5 shift-count source"}],"ordering":["Snapshot both sources before the destination effect so aliases and T/U publication use pre-instruction values.","Publish the result, then advance TPC by four bytes."],"standalone_opcode":true,"state_effects":["Compute the arithmetic right shift using the low six bits of the snapshotted SrcR. The PTO_XLEN result is written unchanged.","Destination codes 0 and 24..29 discard, code 30 pushes U, code 31 pushes T, and codes 1..23 write GPRs; source queues are non-consuming.","No memory, reservation, descriptor, flag, block, privilege, or control-flow state changes except the successful TPC advance."]},"depends_on":["PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"],"id":"PTO-SCALAR-SRA","mnemonic":"SRA","summary":"SRA performs a arithmetic right shift of the PTO_XLEN source by the low six bits of the snapshotted SrcR; the XLEN result is published directly.","surface":"scalar"}// PTO-REVIEW: {"review_method":"formal-definition-read","outcome":"FORMAL-COMPLETE","reviewed_fields":["assembly","encoding","defaults","operation","state","memory","ordering","faults","reserved"]}// NDF-BEGIN: PTO-SRA-ADR-CONTRACT-001// ndf: kind=contract level=L1 layer=scalar status=accepted// Decisions: ADR-0026.// SRA MUST snapshot its scalar sources, apply its mnemonic-owned// width, immediate, modifier, and wrapping rule, then publish through the// assigned destination or commit effect in alias-safe order.// NDF-END: PTO-SRA-ADR-CONTRACT-001// DOC-BEGIN: decodereadonly func InstructionContractOperation_SRA() => ScalarOperationbegin return ScalarOperation_SRA;end;// DOC-END: decode// DOC-BEGIN: operationreadonly func InstructionContractHandler_SRA() => ScalarSemanticHandlerbegin return ScalarHandler_ScalarBinary;end;
pure func InstructionContractShiftAmount_SRA(right: Word) => integer {0..63}begin return UInt(right[5:0]);end;
pure func InstructionContractResult_SRA(left: Word, right: Word) => Wordbegin let amount = InstructionContractShiftAmount_SRA(right); let shifted = ASR(left, amount); return shifted;end;
pure func InstructionContractIsWordOperation_SRA() => booleanbegin return FALSE;end;// DOC-END: operation
SRA is a 32-bit scalar ALU instruction. It arithmetically shifts the source right under the complete XLEN value shift rules; its current instruction contract defines the result publication path and any additional state effect.
Execution snapshots the encoded inputs, then arithmetically shifts the source right under the complete XLEN value shift rules, and only afterward performs the destination effects.
RegDst field selects the Reg5 result target or discards the result.SrcL field selects the scalar value through Reg5.SrcR field selects the register shift count through Reg5.These roles come from the current instruction contract. T/U sources are read and snapshotted without being removed from their queues; exact encoded-zero meanings appear in the generated defaults below.
Every scalar source is snapshotted before the destination effect. The completed value is then routed through RegDst using the current scalar destination map.
This ALU operation has no memory effect. After its successful architectural effects, TPC advances by 4 bytes.
The operation does not introduce a hidden scalar publication target or an implicit memory access. Architectural changes remain limited to the state effects enumerated by the current contract.
Register shifting uses only the low 6 right-source bits, so the effective amount is 0..63; every result is defined at the fixed width.
The generated legality table is authoritative for assigned field values, reserved encodings, and destination discard codes. Decode and source availability are checked before architectural effects.
This example illustrates the current ASL owner and does not replace the normative operation.
For a small SRA example, source -8 shifted arithmetically right by 2 produces -2.
Bodies come from owning ASL. Dragging or buttons change only this page-session view order.
Decisions: ADR-0026. SRA MUST snapshot its scalar sources, apply its mnemonic-owned width, immediate, modifier, and wrapping rule, then publish through the assigned destination or commit effect in alias-safe order.
PTO-SRA-ADR-CONTRACT-001asl/scalar/alu/SRA.asl6e7b0c64c23a1c5334f28e0991534a7cb920a9699b78764274430e0d24d2d22a3db0e01b0aa4e903cbc8f6f774099721877a8a80dcc1c4941eb418b5275694c111 matching entries
PTO-AVS-SCALAR-SRA-DECODE-001tests/asl/scalar/alu/SRA/scalar-decode-sra-canonical-001.asl012741dd3e09501d39b20a921dd4bf853236f81037837bb853559de64013afe6PTO-AVS-SCALAR-SRA-MASKED-001tests/asl/scalar/alu/SRA/scalar-bound-sra-masked-001.asl2ea923a596066c03e8cc36f3d5d455076570d8068ae2d05567077ea5ff26049bPTO-AVS-SCALAR-SRA-MAXIMUM-001tests/asl/scalar/alu/SRA/scalar-exec-sra-maximum-001.asl90ede51e869fb004f4a1e072c6880ec7c89f8ff7c8d2bde4cccf12a7c28daf33PTO-EVIDENCE-RELEASE-TRACEABILITYPTO-EVIDENCE-RELEASE-TRACEABILITYspec/evidence/release-traceability-readiness.jsonc7327021d39dc67ac5564bc55073b3870a397d79ac8d9648284d56e33bc14a3ePTO-EVIDENCE-INSTRUCTION-CONTRACT-CLOSUREPTO-EVIDENCE-INSTRUCTION-CONTRACT-CLOSUREspec/evidence/instruction-contract-closure.json3ef2bb62421c79dff8fa77a1c7983923b523244b8090812883ef81286ca8106aPTO-EVIDENCE-ARCHITECTURE-READINESSPTO-EVIDENCE-ARCHITECTURE-READINESSspec/evidence/architecture-readiness.json4b0b85199101251bea744e0f3591cc31906909dc80d5ab651c417a936036a004PTO-EVIDENCE-RELEASE-GATE-READINESSPTO-EVIDENCE-RELEASE-GATE-READINESSspec/evidence/release-gate-readiness.jsona0f4d2b6920c08981ea55fd8ef820708a40d4feb5402c5150e8e9ab532d84ce0PTO-EVIDENCE-RELEASE-MANIFESTPTO-EVIDENCE-RELEASE-MANIFESTspec/release-manifest.json1a64c109ed7a90351c41e2a418b3c0ebaf8ad975838986d2101385186b85c0d8Loading ADR-0026…
ADR-0026docs/status/decisions/0026-scalar-alu-totality-and-alias-order.md41d126f224dddc371832120f1b02eab64e426872fdcbea452bad77c90bdec349Loading ADR-0059…
ADR-0059docs/status/decisions/0059-mnemonic-field-encoding-closure.mdf18d13f735cfaf9f2803c754c5818f4af33d1cc42c489f0d9ce060b07bb3a196Loading ADR-0084…
ADR-0084docs/status/decisions/0084-scalar-system-and-queue-operations.mde068992fa81e2c4ac46e492391a2f784141d68e041bf0b9e0586c37217d1e08c{
"classification": [
"alu"
],
"documentation": "docs/scalar/alu/SRA.md",
"id": "PTO-SCALAR-SRA",
"instruction_contract": {
"artifact": "spec/evidence/instruction-contract-closure.json",
"mnemonic": "SRA",
"ndf_clause": "PTO-INST-SCALAR-SRA"
},
"mnemonic": "SRA",
"readiness_subjects": [
"ADR-0026",
"ADR-0059",
"ADR-0084"
],
"semantic_tests": [
"PTO-AVS-SCALAR-SRA-MASKED-001",
"PTO-AVS-SCALAR-SRA-MAXIMUM-001"
],
"source": "asl/scalar/alu/SRA.asl",
"surface": "scalar",
"tests": [
"PTO-AVS-SCALAR-SRA-DECODE-001",
"PTO-AVS-SCALAR-SRA-MASKED-001",
"PTO-AVS-SCALAR-SRA-MAXIMUM-001"
]
}0.58.5 · Release candidate7dc8b7e5b121d2b2499a2273bebff29e2cd868126e7b0c64c23a1c5334f28e0991534a7cb920a9699b78764274430e0d24d2d22a618bf9ff3d15933525d357f14229f939fc2ca5750d7b635c037fbe08bfc189cdasl/scalar/alu/SRA.aslasl/scalar/alu/SRA.aslasl/scalar/alu/SRA.asl