HL.REMW

1// PTO-INSTRUCTION: {"assembly":["hl.remw SrcL, SrcR, ->Dst0, Dst1"],"block":[],"catalog_indices":[235],"catalog_records":[{"asm":"hl.remw SrcL, SrcR, ->Dst0, Dst1","constraints":[],"encoding":[{"index":0,"mask":"0xfe00707f07ff","match":"0x00006057000e","width_bits":48}],"encoding_kind":"HL48","fields":[{"name":"RegDst0","pieces":[{"instruction_lsb":23,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"RegDst1","pieces":[{"instruction_lsb":11,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcL","pieces":[{"instruction_lsb":31,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcR","pieces":[{"instruction_lsb":36,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5}],"form_id":"hl_remw_48_3acb485d39a7","length_bits":48,"mnemonic":"HL.REMW","semantic_family":"ALU","semantic_group":"ALU","semantic_handler":"ExecuteScalarRemainderPairW","semantic_summary":"HL.REMW computes a signed low-32-bit remainder/quotient pair from source snapshots, then publishes remainder followed by quotient.","status":"accepted"}],"classification":["alu"],"contract":{"block_composition":["none"],"canonical_assembly":["hl.remw SrcL, SrcR, ->Dst0, Dst1"],"defaults":["SrcL, SrcR, RegDst0, and RegDst1 are required encoded fields; no field can be omitted.","There is no encoded arithmetic mode or implicit operand. The mnemonic fixes signedness and operand width; every HL division/remainder spelling returns both quotient and remainder."],"encoding_class":"standalone-encoded","examples":["hl.remw a0, a1, ->a2, a3","hl.remw t#1, zero, ->u, u"],"exceptions":["Division and remainder are total: zero divisors and signed minimum divided by negative one do not raise an arithmetic exception.","An unavailable selected T/U source raises Fault_IllegalInstruction before either destination effect and before TPC advances."],"field_contracts":{},"field_zero_meanings":{"RegDst0":"Encoded zero discards the remainder.","RegDst1":"Encoded zero discards the quotient.","SrcL":"Encoded zero reads the architectural zero GPR dividend.","SrcR":"Encoded zero reads the architectural zero GPR divisor and therefore selects defined zero-divisor pair results."},"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.","Each destination independently uses the common map: codes 0 and 24..29 discard, codes 1..23 write GPRs, code 30 pushes U, and code 31 pushes T. Duplicate destinations are legal.","Every value of each Reg5 selector is assigned; fixed encoding bits must match the canonical 48-bit form."],"memory_effects":["none"],"operands":[{"field":"RegDst0","role":"remainder Reg5 destination or discard"},{"field":"RegDst1","role":"quotient Reg5 destination or discard"},{"field":"SrcL","role":"dividend Reg5 source"},{"field":"SrcR","role":"divisor Reg5 source"}],"ordering":["Snapshot both sources and compute both results before either destination effect.","Publish remainder to RegDst0, publish quotient to RegDst1, then advance TPC by six bytes."],"standalone_opcode":true,"state_effects":["Interpret the selected operands as signed values, compute both quotient and remainder using the fixed total division rules. For W forms, use the low 32 bits and sign-extend each 32-bit result to XLEN.","A zero divisor returns quotient zero and the effective dividend as remainder. Signed minimum divided by negative one returns signed minimum quotient and zero remainder.","Publish RegDst0 remainder first, then RegDst1 quotient. If both destinations name one GPR, quotient is final; if both push one queue, quotient is newest and remainder is next-newest.","No memory, reservation, descriptor, numeric-status, block, privilege, branch-target, or other control state changes. Successful execution advances TPC by six bytes."]},"depends_on":["PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"],"id":"PTO-SCALAR-HL-REMW","mnemonic":"HL.REMW","summary":"HL.REMW computes a signed low-32-bit remainder/quotient pair from source snapshots, then publishes remainder followed by quotient.","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-HL-REMW-RESULT-ORDER-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// HL.REMW MUST snapshot both sources before destination effects.6// RegDst0 MUST receive the remainder before RegDst1 receives the quotient.7// Duplicate destinations and queue pushes MUST preserve that write order.8// Zero-divisor, signed-overflow, selector, and retirement behavior MUST remain9// identical to the corresponding quotient/remainder arithmetic contract.10// NDF-END: PTO-HL-REMW-RESULT-ORDER-00111// DOC-BEGIN: decode12readonly func InstructionContractOperation_HL_REMW() => ScalarOperation13begin14    return ScalarOperation_HL_REMW;15end;16// DOC-END: decode17// DOC-BEGIN: operation18readonly func InstructionContractHandler_HL_REMW() => ScalarSemanticHandler19begin20    return ScalarHandler_ExecuteScalarRemainderPairW;21end;22pure func InstructionContractQuotient_HL_REMW(23    dividend: Word,24    divisor: Word)25    => Word26begin27    return ScalarDivideSignedW(28        dividend,29        divisor);30end;31
32pure func InstructionContractRemainder_HL_REMW(33    dividend: Word,34    divisor: Word)35    => Word36begin37    return ScalarRemainderSignedW(38        dividend,39        divisor);40end;41
42pure func InstructionContractDst0_HL_REMW(43    dividend: Word,44    divisor: Word)45    => Word46begin47    return InstructionContractRemainder_HL_REMW(48        dividend,49        divisor);50end;51
52pure func InstructionContractDst1_HL_REMW(53    dividend: Word,54    divisor: Word)55    => Word56begin57    return InstructionContractQuotient_HL_REMW(58        dividend,59        divisor);60end;61// DOC-END: operation62