HL.REMU

1// PTO-INSTRUCTION: {"assembly":["hl.remu SrcL, SrcR, ->Dst0, Dst1"],"block":[],"catalog_indices":[233],"catalog_records":[{"asm":"hl.remu SrcL, SrcR, ->Dst0, Dst1","constraints":[],"encoding":[{"index":0,"mask":"0xfe00707f07ff","match":"0x00005057000e","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_remu_48_3bf4e5a663c1","length_bits":48,"mnemonic":"HL.REMU","semantic_family":"ALU","semantic_group":"ALU","semantic_handler":"ExecuteScalarRemainderPair","semantic_summary":"HL.REMU computes an unsigned XLEN remainder/quotient pair from source snapshots, then publishes remainder followed by quotient.","status":"accepted"}],"classification":["alu"],"contract":{"block_composition":["none"],"canonical_assembly":["hl.remu 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.remu a0, a1, ->a2, a3","hl.remu 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 unsigned values, compute both quotient and remainder using the fixed total division rules.","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-REMU","mnemonic":"HL.REMU","summary":"HL.REMU computes an unsigned XLEN 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-REMU-RESULT-ORDER-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// HL.REMU 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-REMU-RESULT-ORDER-00111// DOC-BEGIN: decode12readonly func InstructionContractOperation_HL_REMU() => ScalarOperation13begin14    return ScalarOperation_HL_REMU;15end;16// DOC-END: decode17// DOC-BEGIN: operation18readonly func InstructionContractHandler_HL_REMU() => ScalarSemanticHandler19begin20    return ScalarHandler_ExecuteScalarRemainderPair;21end;22pure func InstructionContractQuotient_HL_REMU(23    dividend: Word,24    divisor: Word)25    => Word26begin27    return ScalarDivideUnsigned(28        dividend,29        divisor);30end;31
32pure func InstructionContractRemainder_HL_REMU(33    dividend: Word,34    divisor: Word)35    => Word36begin37    return ScalarRemainderUnsigned(38        dividend,39        divisor);40end;41
42pure func InstructionContractDst0_HL_REMU(43    dividend: Word,44    divisor: Word)45    => Word46begin47    return InstructionContractRemainder_HL_REMU(48        dividend,49        divisor);50end;51
52pure func InstructionContractDst1_HL_REMU(53    dividend: Word,54    divisor: Word)55    => Word56begin57    return InstructionContractQuotient_HL_REMU(58        dividend,59        divisor);60end;61// DOC-END: operation62