REM

assembly

[
  "rem SrcL, SrcR, ->{t, u, Rd}"
]

block

[]

catalog_indices

[
  372
]

catalog_records

[
  {
    "asm": "rem SrcL, SrcR, ->{t, u, Rd}",
    "constraints": [],
    "encoding": [
      {
        "index": 0,
        "mask": "0xfe00707f",
        "match": "0x00004057",
        "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": "rem_32_0abbd6a3b865",
    "length_bits": 32,
    "mnemonic": "REM",
    "semantic_family": "ALU",
    "semantic_group": "ALU",
    "semantic_handler": "ScalarRemainderSigned",
    "semantic_summary": "REM computes the signed XLEN remainder using total fixed-width semantics and publishes the XLEN result.",
    "status": "accepted"
  }
]

classification

[
  "alu"
]

contract

{
  "block_composition": [
    "none"
  ],
  "canonical_assembly": [
    "rem SrcL, SrcR, ->{t, u, Rd}"
  ],
  "defaults": [
    "SrcL, SrcR, and RegDst are required encoded fields; no field can be omitted.",
    "There is no encoded arithmetic mode or implicit operand. The mnemonic fixes signedness, operand width, and quotient-versus-remainder selection."
  ],
  "encoding_class": "standalone-encoded",
  "examples": [
    "rem a0, a1, ->a2",
    "rem t#1, zero, ->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 the destination effect and before TPC advances."
  ],
  "field_contracts": {},
  "field_zero_meanings": {
    "RegDst": "Encoded zero discards the result.",
    "SrcL": "Encoded zero reads the architectural zero GPR dividend.",
    "SrcR": "Encoded zero reads the architectural zero GPR divisor and therefore selects the defined zero-divisor result."
  },
  "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, codes 1..23 write GPRs, code 30 pushes U, and code 31 pushes T.",
    "Every value of each Reg5 selector is assigned; fixed encoding bits must match the canonical form."
  ],
  "memory_effects": [
    "none"
  ],
  "operands": [
    {
      "field": "RegDst",
      "role": "Reg5 destination or discard"
    },
    {
      "field": "SrcL",
      "role": "dividend Reg5 source"
    },
    {
      "field": "SrcR",
      "role": "divisor Reg5 source"
    }
  ],
  "ordering": [
    "Snapshot both sources before the destination effect so duplicate selectors and destination aliases observe pre-instruction values.",
    "Publish the result, then advance TPC by four bytes."
  ],
  "standalone_opcode": true,
  "state_effects": [
    "Interpret both complete XLEN sources as signed two-complement integers and return dividend minus the quotient-truncated-toward-zero times divisor.",
    "A zero divisor returns the unchanged dividend. Signed minimum divided by negative one returns zero.",
    "Publish the complete XLEN result through the common Reg5 destination map. Relative sources are non-consuming; only a T or U destination push changes a temporary queue.",
    "No memory, reservation, descriptor, numeric-status, block, privilege, branch-target, or other control state changes. Successful execution advances TPC by four bytes."
  ]
}

depends_on

[
  "PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"
]

id

PTO-SCALAR-REM

mnemonic

REM

summary

REM computes the signed XLEN remainder using total fixed-width semantics and publishes the XLEN result.

surface

scalar

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