PTO-SCALAR-MODEL-SYS-SEMANTICS

1// PTO-UNIT: {"id":"PTO-SCALAR-MODEL-SYS-SEMANTICS","surface":"scalar","classification":["model","sys","semantics"],"depends_on":["PTO-SCALAR-MODEL-AMO-SEMANTICS","PTO-BLOCK-MODEL-STATE-BARG"]}2// PTO-REQ-SCALAR-SYS-001, PTO-REQ-MEMORY-TSO-001: PTO base SSR access,3// architectural time, and data/instruction fences.4
5impdef func ReadMonotonicTime() => Word6begin7    // The default executable model uses the monotonically increasing cycle8    // state. Implementations may override this with a nanosecond time source.9    return _SystemRegisters.cycle;10end;11
12func AdvanceArchitecturalTime()13begin14    // PTO v0 defines one time unit per decoded execution attempt.15    _SystemRegisters.cycle = _SystemRegisters.cycle + 1;16end;17
18// PTO-REQ-EXECUTION-STATUS-001: each public decoded execution boundary starts19// a fresh result attempt without erasing the visible trap-bank record.20func BeginArchitecturalInstructionAttempt()21begin22    _LastFault = Fault_None;23    _FaultAddress = Zeros{PTO_XLEN};24    AdvanceArchitecturalTime();25end;26
27func ReadSystemRegister(reg: SystemRegister) => Word28begin29    case reg of30        when SystemRegister_THREAD_PTR => return _SystemRegisters.thread_ptr;31        when SystemRegister_GLOBAL_PTR => return _SystemRegisters.global_ptr;32        when SystemRegister_TIME     => return ReadMonotonicTime();33        when SystemRegister_CORE_STATE => return _SystemRegisters.core_state;34        when SystemRegister_CORE_ID  => return _SystemRegisters.core_id;35        when SystemRegister_THREAD_ID => return _SystemRegisters.thread_id;36        when SystemRegister_VENDOR   => return _SystemRegisters.vendor;37        when SystemRegister_VERSION  => return _SystemRegisters.version;38        when SystemRegister_CORE_FEATURE => return _SystemRegisters.core_feature;39        when SystemRegister_CORE_FEATURE_ENABLE =>40            return _SystemRegisters.core_feature_enable;41        when SystemRegister_TILE_CAPACITY => return _SystemRegisters.tile_capacity;42        when SystemRegister_BLOCKNUM => return _SystemRegisters.blocknum;43        when SystemRegister_BLOCKID  => return _SystemRegisters.blockid;44        when SystemRegister_CYCLE    => return _SystemRegisters.cycle;45    end;46end;47
48func SystemRegisterIsWritable(reg: SystemRegister) => boolean49begin50    return reg == SystemRegister_THREAD_PTR ||51           reg == SystemRegister_GLOBAL_PTR ||52           reg == SystemRegister_CORE_STATE ||53           reg == SystemRegister_CORE_FEATURE_ENABLE;54end;55
56func WriteSystemRegister(reg: SystemRegister, value: Word)57begin58    if !SystemRegisterIsWritable(reg) then59        SetFault(Fault_IllegalInstruction, ReadPC());60        return;61    end;62    case reg of63        when SystemRegister_THREAD_PTR => _SystemRegisters.thread_ptr = value;64        when SystemRegister_GLOBAL_PTR => _SystemRegisters.global_ptr = value;65        when SystemRegister_CORE_STATE =>66            _SystemRegisters.core_state = value;67            _CurrentACR = UInt(value[3:0]) as AccessControlRing;68        when SystemRegister_CORE_FEATURE_ENABLE =>69            _SystemRegisters.core_feature_enable = value;70        otherwise => assert FALSE;71    end;72end;73
74func FenceData(predecessor: bits(4), successor: bits(4))75begin76    _ReservationValid = FALSE;77    _LastFencePredecessor = predecessor;78    _LastFenceSuccessor = successor;79    if predecessor[3] == '1' || successor[3] == '1' then80        _InstructionCacheEpoch = _InstructionCacheEpoch + 1;81    end;82    RecordDataFenceEvent(predecessor, successor);83end;84
85func FenceInstruction()86begin87    _ReservationValid = FALSE;88    // The executable byte-array model has coherent instruction/data storage.89    // The epoch makes the architectural visibility point explicit.90    _InstructionCacheEpoch = _InstructionCacheEpoch + 1;91end;92
93func SoftwareBreakpoint(tag: bits(5))94begin95    SetFaultWithCause(96        Fault_SoftwareBreakpoint,97        ReadPC(),98        ZeroExtend{24}(tag));99end;100
101func SwapSystemRegister(reg: SystemRegister, value: Word) => Word102begin103    let old_value = ReadSystemRegister(reg);104    if SystemRegisterIsWritable(reg) then WriteSystemRegister(reg, value);105    else SetFault(Fault_IllegalInstruction, ReadPC());106    end;107    return old_value;108end;109
110pure func IsCanonicalAddress48(address: Word) => boolean111begin112    if address[47] == '0' then return address[63:48] == Zeros{16};113    else return address[63:48] == Ones{16};114    end;115end;116
117pure func MaintenanceAccessPermitted(operation: MaintenanceOperation,118                                     ring: AccessControlRing) => boolean119begin120    // Cache maintenance is a local hint in PTO v0. Translation maintenance is121    // manager state and is therefore restricted to the root access ring.122    case operation of123        when Maintenance_TLB_IV, Maintenance_TLB_IAV,124             Maintenance_TLB_IA, Maintenance_TLB_IALL => return ring == 0;125        otherwise => return TRUE;126    end;127end;128
129func ExecuteMaintenance(operation: MaintenanceOperation, operand: Word)130begin131    if !MaintenanceAccessPermitted(operation, CurrentACR()) then132        SetFault(Fault_IllegalInstruction, ReadPC());133        return;134    end;135    case operation of136        when Maintenance_DC_IALL, Maintenance_DC_IVA, Maintenance_DC_ISW,137             Maintenance_DC_ZVA, Maintenance_DC_CVA, Maintenance_DC_CIVA,138             Maintenance_DC_CSW, Maintenance_DC_CISW =>139            _DataCacheEpoch = _DataCacheEpoch + 1;140        when Maintenance_IC_IALL, Maintenance_IC_IVA =>141            _InstructionCacheEpoch = _InstructionCacheEpoch + 1;142        when Maintenance_BC_IALL, Maintenance_BC_IVA =>143            _BundleCacheEpoch = _BundleCacheEpoch + 1;144        when Maintenance_TLB_IV, Maintenance_TLB_IAV =>145            if !IsCanonicalAddress48(operand) then146                SetFault(Fault_DataPage, operand);147            else148                _TLBEpoch = _TLBEpoch + 1;149            end;150        when Maintenance_TLB_IA =>151            if operand[63:16] != Zeros{48} then152                SetFault(Fault_IllegalInstruction, ReadPC());153            else154                _TLBEpoch = _TLBEpoch + 1;155            end;156        when Maintenance_TLB_IALL => _TLBEpoch = _TLBEpoch + 1;157    end;158    if _LastFault == Fault_None then159        // Epochs are the executable PTO-v0 completion effect; retaining the160        // exact operation and operand makes scope-token handling auditable.161        _LastMaintenanceOperation = operation;162        _LastMaintenanceOperand = operand;163    end;164end;165
166func ArchitectureAssert(value: Word)167begin168    if IsZero(value) then SetFault(Fault_Assert, ReadPC()); end;169end;170
171func ExecuteLocalStateRegisterGet(destination: Reg5Selector,172                                  identifier: bits(12))173begin174    if !CurrentBARGWordApplicable(identifier) then175        SetFault(Fault_BundleControl, ReadTPC());176        return;177    end;178    let value = ReadCurrentBARGWord(identifier);179    WriteScalarDestination(destination, value);180end;181
182func BundleTransformHint()183begin184    _BundleHintEpoch = _BundleHintEpoch + 1;185end;186
187func ArchitectureCloseRequest(request_type: bits(4))188begin189    if !ServiceRequestPermitted(CurrentACR(), request_type) then190        SetFault(Fault_IllegalInstruction, ReadTPC());191        return;192    end;193    _SystemBlockTerminalPending = TRUE;194    if RaiseServiceRequest(request_type) then195        _ArchitectureRequestEpoch = _ArchitectureRequestEpoch + 1;196        _ControlRequestOperand[3:0] = request_type;197    end;198end;199
200func ArchitectureEnterRequest(request_type: bits(4))201begin202    // Request types 0 and 1 are architectural aliases in PTO v0. Both restore203    // the same complete visible snapshot; a future profile must use a distinct204    // identity before assigning different recovery behavior.205    if request_type != '0000' && request_type != '0001' then206        SetFault(Fault_IllegalInstruction, ReadPC());207        return;208    end;209    let target = CurrentACR();210    let recovery_context = _TrapContexts[[target]];211    if !TrapContextRecoverable(target) then212        SetFault(Fault_ExecutionStateCheck, ReadPC());213        if recovery_context.valid then214            _TrapContexts[[target]] = recovery_context;215        end;216        return;217    end;218    if !CompleteBundleAt(_BundleSequentialPC) then219        _TrapContexts[[target]] = recovery_context;220        return;221    end;222    let recovered = RecoverTrapContext(target);223    assert recovered;224    _ArchitectureRequestEpoch = _ArchitectureRequestEpoch + 1;225    _ControlRequestOperand[3:0] = request_type;226end;227
228readonly func IsSystemBlockScalarOperation(operation: ScalarOperation)229    => boolean230begin231    case operation of232        when ScalarOperation_ACRC, ScalarOperation_ACRE,233             ScalarOperation_ASSERT,234             ScalarOperation_BC_IALL, ScalarOperation_BC_IVA,235             ScalarOperation_BSE, ScalarOperation_BWE,236             ScalarOperation_BWI, ScalarOperation_BWT,237             ScalarOperation_C_EBREAK, ScalarOperation_C_SSRGET,238             ScalarOperation_DC_CISW, ScalarOperation_DC_CIVA,239             ScalarOperation_DC_CSW, ScalarOperation_DC_CVA,240             ScalarOperation_DC_IALL, ScalarOperation_DC_ISW,241             ScalarOperation_DC_IVA, ScalarOperation_DC_ZVA,242             ScalarOperation_EBREAK,243             ScalarOperation_FENCE_D, ScalarOperation_FENCE_I,244             ScalarOperation_HL_SSRGET, ScalarOperation_HL_SSRSET,245             ScalarOperation_IC_IALL, ScalarOperation_IC_IVA,246             ScalarOperation_SSRGET, ScalarOperation_SSRSET,247             ScalarOperation_SSRSWAP,248             ScalarOperation_TLB_IA, ScalarOperation_TLB_IALL,249             ScalarOperation_TLB_IAV, ScalarOperation_TLB_IV =>250            return TRUE;251        otherwise =>252            return FALSE;253    end;254end;255
256func ExecuteControlRequest(request: ExecutionControlRequest, operand: Word)257begin258    // PTO v0 exposes a nonblocking scheduling handoff. BSE/BWE/BWI/BWT retire259    // after publishing the exact request and operand; suspension and wakeup do260    // not add architecture-visible state in this reference profile.261    _LastControlRequest = request;262    _ControlRequestOperand = operand;263    _ArchitectureRequestEpoch = _ArchitectureRequestEpoch + 1;264end;265
266readonly func BundleCommitTargetWritable() => boolean267begin268    return _BundleActive &&269           (_BARG.block_type == BundleKind_Standard ||270            _BARG.block_type == BundleKind_Floating);271end;272
273readonly func IsCommitConditionSetter(operation: ScalarOperation)274    => boolean275begin276    case operation of277        when ScalarOperation_C_SETC_EQ, ScalarOperation_C_SETC_NE,278             ScalarOperation_SETC_EQ, ScalarOperation_SETC_NE,279             ScalarOperation_SETC_LT, ScalarOperation_SETC_GE,280             ScalarOperation_SETC_LTU, ScalarOperation_SETC_GEU,281             ScalarOperation_SETC_EQI, ScalarOperation_SETC_NEI,282             ScalarOperation_SETC_LTI, ScalarOperation_SETC_GEI,283             ScalarOperation_SETC_LTUI, ScalarOperation_SETC_GEUI,284             ScalarOperation_SETC_AND, ScalarOperation_SETC_OR,285             ScalarOperation_SETC_ANDI, ScalarOperation_SETC_ORI,286             ScalarOperation_HL_SETC_EQI, ScalarOperation_HL_SETC_NEI,287             ScalarOperation_HL_SETC_LTI, ScalarOperation_HL_SETC_GEI,288             ScalarOperation_HL_SETC_LTUI, ScalarOperation_HL_SETC_GEUI,289             ScalarOperation_HL_SETC_ANDI, ScalarOperation_HL_SETC_ORI =>290            return TRUE;291        otherwise =>292            return FALSE;293    end;294end;295
296readonly func ScalarOperationApplicable(operation: ScalarOperation)297    => boolean298begin299    if _SystemBlockTerminalPending then300        return FALSE;301    end;302    if IsCommitConditionSetter(operation) then303        return _BundleActive &&304               _BundleBodyActive &&305               _BARG.transfer_type == BundleTransfer_Conditional &&306               !_BundleConditionSet;307    end;308    case operation of309        when ScalarOperation_C_SETC_TGT =>310            return BundleCommitTargetWritable() &&311                   !_BundleCommitTargetSet;312        when ScalarOperation_SETC_TGT =>313            return BundleCommitTargetWritable();314        when ScalarOperation_LSRGET =>315            return _BundleActive && _BundleBodyActive;316        otherwise =>317            if IsSystemBlockScalarOperation(operation) then318                return _BundleActive &&319                       _BundleBodyActive &&320                       _BARG.block_type == BundleKind_System;321            else322                return TRUE;323            end;324    end;325end;326
327func SetCommitTarget(value: Word)328begin329    if !BundleCommitTargetWritable() then330        SetFault(Fault_BundleControl, ReadTPC());331        return;332    end;333    _BARG.bpcn = value;334end;335
336func SetCompressedCommitTarget(value: Word)337begin338    if !BundleCommitTargetWritable() || _BundleCommitTargetSet then339        SetFault(Fault_BundleControl, ReadTPC());340        return;341    end;342    _BARG.bpcn = value;343    _BundleCommitTargetSet = TRUE;344end;345