TLB.IAV

1// PTO-INSTRUCTION: {"assembly":["tlb.iav SrcL"],"block":[],"catalog_indices":[459],"catalog_records":[{"asm":"tlb.iav SrcL","constraints":[],"encoding":[{"index":0,"mask":"0xfff07fff","match":"0x0020702b","width_bits":32}],"encoding_kind":"L32","fields":[{"name":"SrcL","pieces":[{"instruction_lsb":15,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5}],"form_id":"tlb_iav_32_95f4937d2917","length_bits":32,"mnemonic":"TLB.IAV","semantic_family":"SYS","semantic_group":"SYS","semantic_handler":"ExecuteMaintenance","semantic_summary":"TLB.IAV completes the canonical 48-bit virtual address with ASID scope maintenance operation synchronously.","status":"accepted"}],"classification":["sys"],"contract":{"block_composition":["TLB.IAV executes as one scalar operation in the body of an active SYS block."],"canonical_assembly":["tlb.iav SrcL"],"defaults":["Every displayed operand is encoded explicitly. Encoded zero is an assigned value and never denotes omission."],"encoding_class":"standalone-encoded","examples":["tlb.iav SrcL"],"exceptions":["Invalid block placement raises Illegal Block Exception before encoded-field legality or effects.","A reserved encoding or rejected access raises Illegal Instruction before destination, queue, system-state, or TPC effects."],"field_contracts":{},"field_zero_meanings":{"SrcL":"Encoded zero names the architectural zero GPR."},"legality":["Every fixed bit and explicit field constraint is checked before operation semantics.","TLB maintenance is assigned only at ACR0 and rejects at every other ring before operand validation.","The operand must be a canonical 48-bit virtual address."],"memory_effects":["No ordinary scalar memory access is performed; success records the operation and operand and advances the selected maintenance epoch."],"operands":[{"field":"SrcL","role":"Reg5 source: R0..R23, T#1..T#4, or U#1..U#4"}],"ordering":["Check block placement and encoded legality before source reads or architectural effects.","Snapshot every scalar source before the selected system effect, then advance TPC only after success."],"standalone_opcode":true,"state_effects":["Success records Maintenance_TLB_IAV and its exact operand token.","Success advances exactly one data-cache, instruction-cache, bundle-cache, or TLB epoch and then advances TPC."]},"depends_on":["PTO-SCALAR-MODEL-SYS-SEMANTICS"],"id":"PTO-SCALAR-TLB-IAV","mnemonic":"TLB.IAV","summary":"TLB.IAV completes the canonical 48-bit virtual address with ASID scope maintenance operation synchronously.","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-TLB-IAV-ADR-CONTRACT-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// Decisions: ADR-0031.6// TLB.IAV MUST enforce its mnemonic-owned system or maintenance access7// domain before effects and MUST preserve destination, queue, and system state8// on rejection except for the ordinary instruction-attempt trap envelope.9// NDF-END: PTO-TLB-IAV-ADR-CONTRACT-00110// DOC-BEGIN: decode11readonly func InstructionContractOperation_TLB_IAV()12    => ScalarOperation13begin14    return ScalarOperation_TLB_IAV;15end;16// DOC-END: decode17// DOC-BEGIN: operation18readonly func InstructionContractHandler_TLB_IAV()19    => ScalarSemanticHandler20begin21    return ScalarHandler_ExecuteMaintenance;22end;23
24pure func InstructionContractRequiresSystemBlock_TLB_IAV()25    => boolean26begin27    return TRUE;28end;29
30pure func InstructionContractMaintenanceOperation_TLB_IAV()31    => MaintenanceOperation32begin33    return Maintenance_TLB_IAV;34end;35
36pure func InstructionContractMaintenanceUsesOperand_TLB_IAV()37    => boolean38begin39    return TRUE;40end;41
42pure func InstructionContractMaintenanceRequiresRootRing_TLB_IAV()43    => boolean44begin45    return TRUE;46end;47// DOC-END: operation48