HL.DIV

assembly

[
  "hl.div SrcL, SrcR, ->Dst0, Dst1"
]

block

[]

catalog_indices

[
  137
]

catalog_records

[
  {
    "asm": "hl.div SrcL, SrcR, ->Dst0, Dst1",
    "constraints": [],
    "encoding": [
      {
        "index": 0,
        "mask": "0xfe00707f07ff",
        "match": "0x00000057000e",
        "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_div_48_e8ff1fc1cb98",
    "length_bits": 48,
    "mnemonic": "HL.DIV",
    "semantic_family": "ALU",
    "semantic_group": "ALU",
    "semantic_handler": "ExecuteScalarDividePair",
    "semantic_summary": "HL.DIV computes a signed XLEN quotient/remainder pair from source snapshots, then publishes quotient followed by remainder.",
    "status": "accepted"
  }
]

classification

[
  "alu"
]

contract

{
  "block_composition": [
    "none"
  ],
  "canonical_assembly": [
    "hl.div 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.div a0, a1, ->a2, a3",
    "hl.div 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 quotient.",
    "RegDst1": "Encoded zero discards the remainder.",
    "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": "quotient Reg5 destination or discard"
    },
    {
      "field": "RegDst1",
      "role": "remainder 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 quotient to RegDst0, publish remainder 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.",
    "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 quotient first, then RegDst1 remainder. If both destinations name one GPR, remainder is final; if both push one queue, remainder is newest and quotient 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-DIV

mnemonic

HL.DIV

summary

HL.DIV computes a signed XLEN quotient/remainder pair from source snapshots, then publishes quotient followed by remainder.

surface

scalar

{
  "classification": [
    "alu"
  ],
  "documentation": "docs/scalar/alu/HL.DIV.md",
  "id": "PTO-SCALAR-HL-DIV",
  "instruction_contract": {
    "artifact": "spec/evidence/instruction-contract-closure.json",
    "mnemonic": "HL.DIV",
    "ndf_clause": "PTO-INST-SCALAR-HL-DIV"
  },
  "mnemonic": "HL.DIV",
  "readiness_subjects": [
    "ADR-0026",
    "ADR-0059",
    "ADR-0084"
  ],
  "semantic_tests": [
    "PTO-AVS-SCALAR-HL-DIV-PAIR-001"
  ],
  "source": "asl/scalar/alu/HL.DIV.asl",
  "surface": "scalar",
  "tests": [
    "PTO-AVS-SCALAR-HL-DIV-DECODE-001",
    "PTO-AVS-SCALAR-HL-DIV-PAIR-001"
  ]
}