HL.ADDTPC

1// PTO-INSTRUCTION: {"assembly":["hl.addtpc imm, ->{t, u, Rd}"],"block":[],"catalog_indices":[119],"catalog_records":[{"asm":"hl.addtpc imm, ->{t, u, Rd}","constraints":[{"field":"RegDst","operator":"not-equal","value":10}],"encoding":[{"index":0,"mask":"0x0000007f000f","match":"0x00000007000e","width_bits":48}],"encoding_kind":"HL48","fields":[{"name":"RegDst","pieces":[{"instruction_lsb":23,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"imm32","pieces":[{"instruction_lsb":28,"value_lsb":0,"width":20},{"instruction_lsb":4,"value_lsb":20,"width":12}],"signedness":"encoding-defined","width":32}],"form_id":"hl_addtpc_48_2e8e692eea09","length_bits":48,"mnemonic":"HL.ADDTPC","semantic_family":"BRU","semantic_group":"BRU","semantic_handler":"AddToPC","semantic_summary":"HL.ADDTPC - Add a signed 4 KiB page displacement to the current TPC.","status":"accepted"}],"classification":["bru"],"contract":{"block_composition":["none"],"canonical_assembly":["hl.addtpc imm, ->{t, u, Rd}"],"defaults":["The imm32 field is sign-extended and scaled by 4096 bytes; encoded zero contributes a zero page displacement and produces the current instruction TPC.","The selected assembly form determines which fields are present; every present field carries its encoded value and no encoded zero means omission."],"encoding_class":"standalone-encoded","examples":["hl.addtpc imm, ->{t, u, Rd}"],"exceptions":["Reserved field encodings raise Fault_IllegalInstruction before effects; handler-specific arithmetic, memory, control-flow, system-register, and privilege faults follow the embedded normative ASL operation."],"field_contracts":{},"field_zero_meanings":{"RegDst":"Encoded zero names the architectural zero GPR.","imm32":"Encoded zero contributes a zero page displacement and produces the current instruction TPC."},"legality":["hl_addtpc_48_2e8e692eea09.RegDst excludes 10; the excluded encoding is reserved."],"memory_effects":["none"],"operands":[{"field":"RegDst","role":"absolute GPR destination"},{"field":"imm32","role":"signed 32-bit 4 KiB page displacement"}],"ordering":["Read the current instruction TPC before computing the wrapping XLEN result.","After the destination effect, the scalar dispatch boundary advances TPC by six bytes."],"standalone_opcode":true,"state_effects":["HL.ADDTPC writes TPC + (SignExtend(imm32) << 12), wrapping at XLEN, through the selected Reg5 destination.","The instruction does not install a control-flow target and does not directly modify TPC."]},"depends_on":["PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"],"id":"PTO-SCALAR-HL-ADDTPC","mnemonic":"HL.ADDTPC","summary":"HL.ADDTPC - Add a signed 4 KiB page displacement to the current TPC.","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-ADDTPC-PAGE-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// HL.ADDTPC MUST add SignExtend(imm32) shifted left by twelve to the current6// instruction TPC, MUST wrap at XLEN, and MUST write only through the selected7// Reg5 destination. It MUST NOT install a control-flow target or directly8// advance TPC. Encoded immediate zero MUST produce the current TPC.9// NDF-END: PTO-HL-ADDTPC-PAGE-00110// DOC-BEGIN: decode11readonly func InstructionContractOperation_HL_ADDTPC() => ScalarOperation12begin13    return ScalarOperation_HL_ADDTPC;14end;15// DOC-END: decode16// DOC-BEGIN: operation17readonly func InstructionContractHandler_HL_ADDTPC() => ScalarSemanticHandler18begin19    return ScalarHandler_AddToPC;20end;21
22pure func InstructionContractUsesTPC_HL_ADDTPC()23    => boolean24begin25    return TRUE;26end;27
28pure func InstructionContractImmediateWidth_HL_ADDTPC()29    => integer {32}30begin31    return 32;32end;33
34pure func InstructionContractImmediateIsSigned_HL_ADDTPC()35    => boolean36begin37    return TRUE;38end;39
40pure func InstructionContractPageShift_HL_ADDTPC()41    => integer {12}42begin43    return 12;44end;45
46pure func InstructionContractWritesTPC_HL_ADDTPC()47    => boolean48begin49    return FALSE;50end;51
52pure func InstructionContractTarget_HL_ADDTPC(53    base: Word,54    page_offset: Word)55    => Word56begin57    return base + LSL(page_offset, 12);58end;59// DOC-END: operation60