Skip to main content

PTO-ARCH-DATA-TYPES-FORMAT-TF32

PTO-ARCH-DATA-TYPES-FORMAT-TF32

ASL pseudocode

This Operation comes directly from the instruction owner; the page does not rewrite its behavior.

// PTO-REQ-HARDWARE-NUMERIC-001: exact TF32 encoding and finite values.
pure func TF32NumericFormatDescriptor() => NumericFormatDescriptorbegin    return NumericFormatDescriptor {        available = TRUE, kind = NumericFormatKind_FixedBinary,        carrier_bits = 32, lane_bits = 32, lanes_per_carrier = 1,        sign_bits = 1, sign_bit = 31,        exponent_bits_min = 8, exponent_bits_max = 8,        fraction_bits_min = 10, fraction_bits_max = 10,        exponent_bias_available = TRUE, exponent_bias = 127,        required_low_zero_bits = 13, required_high_zero_bits = 0,        has_zero = TRUE, has_signed_zero = TRUE, has_subnormal = TRUE,        has_infinity = TRUE, has_quiet_nan = TRUE,        has_signaling_nan = TRUE    };end;
pure func TF32FiniteDecomposition(value: bits(32))    => (boolean, boolean, Word, integer {-1074..1023})begin    if value[12:0] != Zeros{13} then        return (FALSE, FALSE, Zeros{PTO_XLEN}, 0);    end;    let exponent = value[30:23];    let fraction = value[22:13];    if exponent == Ones{8} then        return (FALSE, FALSE, Zeros{PTO_XLEN}, 0);    elsif exponent == Zeros{8} then        if fraction == Zeros{10} then            return (TRUE, value[31] == '1', Zeros{PTO_XLEN}, 0);        else return (TRUE, value[31] == '1',                     ZeroExtend{PTO_XLEN}(fraction), -136);        end;    else return (TRUE, value[31] == '1',                 LSL(Zeros{PTO_XLEN} + 1, 10) +                     ZeroExtend{PTO_XLEN}(fraction),                 (UInt(exponent) - (127 + 10))                     as integer {-1074..1023});    end;end;
pure func TF32EncodingValid(value: bits(32)) => booleanbegin    return value[12:0] == Zeros{13};end;pure func ClassifyTF32(value: bits(32)) => NumericValueClassbegin    let exponent = value[30:23];    let fraction = value[22:13];    if exponent == Ones{8} then        if fraction == Zeros{10} then            if value[31] == '1' then return NumericValue_NegativeInfinity;            else return NumericValue_PositiveInfinity;            end;        elsif fraction[9] == '1' then return NumericValue_QuietNaN;        else return NumericValue_SignalingNaN;        end;    end;    return NumericValueClassFromFiniteSign(value[31],        exponent == Zeros{8} && fraction == Zeros{10},        exponent == Zeros{8} && fraction != Zeros{10});end;
pure func TF32CanonicalNaN() => Wordbegin    return Zeros{PTO_XLEN} + 0x7fc00000;end;
pure func TF32SignedZeroEncodings() => (Word, Word)begin    return (Zeros{PTO_XLEN}, Zeros{PTO_XLEN} + 0x80000000);end;
View the complete ASL owner
// PTO-UNIT: {"id":"PTO-ARCH-DATA-TYPES-FORMAT-TF32","surface":"arch","classification":["data-types","formats","tf32"],"depends_on":["PTO-ARCH-DATA-TYPES-FORMAT-DESCRIPTOR"]}// DOC-BEGIN: operation// PTO-REQ-HARDWARE-NUMERIC-001: exact TF32 encoding and finite values.
pure func TF32NumericFormatDescriptor() => NumericFormatDescriptorbegin    return NumericFormatDescriptor {        available = TRUE, kind = NumericFormatKind_FixedBinary,        carrier_bits = 32, lane_bits = 32, lanes_per_carrier = 1,        sign_bits = 1, sign_bit = 31,        exponent_bits_min = 8, exponent_bits_max = 8,        fraction_bits_min = 10, fraction_bits_max = 10,        exponent_bias_available = TRUE, exponent_bias = 127,        required_low_zero_bits = 13, required_high_zero_bits = 0,        has_zero = TRUE, has_signed_zero = TRUE, has_subnormal = TRUE,        has_infinity = TRUE, has_quiet_nan = TRUE,        has_signaling_nan = TRUE    };end;
pure func TF32FiniteDecomposition(value: bits(32))    => (boolean, boolean, Word, integer {-1074..1023})begin    if value[12:0] != Zeros{13} then        return (FALSE, FALSE, Zeros{PTO_XLEN}, 0);    end;    let exponent = value[30:23];    let fraction = value[22:13];    if exponent == Ones{8} then        return (FALSE, FALSE, Zeros{PTO_XLEN}, 0);    elsif exponent == Zeros{8} then        if fraction == Zeros{10} then            return (TRUE, value[31] == '1', Zeros{PTO_XLEN}, 0);        else return (TRUE, value[31] == '1',                     ZeroExtend{PTO_XLEN}(fraction), -136);        end;    else return (TRUE, value[31] == '1',                 LSL(Zeros{PTO_XLEN} + 1, 10) +                     ZeroExtend{PTO_XLEN}(fraction),                 (UInt(exponent) - (127 + 10))                     as integer {-1074..1023});    end;end;
pure func TF32EncodingValid(value: bits(32)) => booleanbegin    return value[12:0] == Zeros{13};end;pure func ClassifyTF32(value: bits(32)) => NumericValueClassbegin    let exponent = value[30:23];    let fraction = value[22:13];    if exponent == Ones{8} then        if fraction == Zeros{10} then            if value[31] == '1' then return NumericValue_NegativeInfinity;            else return NumericValue_PositiveInfinity;            end;        elsif fraction[9] == '1' then return NumericValue_QuietNaN;        else return NumericValue_SignalingNaN;        end;    end;    return NumericValueClassFromFiniteSign(value[31],        exponent == Zeros{8} && fraction == Zeros{10},        exponent == Zeros{8} && fraction != Zeros{10});end;
pure func TF32CanonicalNaN() => Wordbegin    return Zeros{PTO_XLEN} + 0x7fc00000;end;
pure func TF32SignedZeroEncodings() => (Word, Word)begin    return (Zeros{PTO_XLEN}, Zeros{PTO_XLEN} + 0x80000000);end;// DOC-END: operation

Architecture behavior

purpose scope

Purpose and scope

This unit defines the exact TF32 carrier contract used by the numeric-format dispatch: descriptor, encoding validity, finite decomposition, classification, canonical NaN, and signed zeros.

It keeps the architectural ten-bit fraction distinct from an arbitrary 32-bit host floating-point value.

concepts state

Concepts and visible state

  • TF32NumericFormatDescriptor uses a 32-bit carrier with one sign bit, eight exponent bits, ten fraction bits, bias 127, and 13 required low zero bits.
  • TF32EncodingValid checks those 13 low bits. TF32FiniteDecomposition then exposes an exact sign, integer significand, and base-two exponent for valid finite values.
  • ClassifyTF32 distinguishes signed zero, signed subnormal, signed normal, signed infinity, quiet NaN, and signaling NaN from the architectural exponent and fraction fields.
rules interactions

Rules and interactions

A carrier with any nonzero bit in [12:0] is invalid for TF32, even if its upper 19 bits resemble a valid value.

Exponent 0xff selects infinity when the ten-bit fraction is zero; otherwise fraction bit 9 distinguishes quiet from signaling NaN.

TF32CanonicalNaN is 0x7fc00000; TF32SignedZeroEncodings returns 0x00000000 and 0x80000000.

boundaries

Architectural boundaries

Finite decomposition reports unavailable for invalid encodings, infinities, and NaNs. The returned placeholder fields are not a numeric result when availability is false.

Bits above the architectural 32-bit carrier are outside this unit; callers pass value[31:0] through the numeric-format dispatcher.

example usage

illustrative reading example

0x3f800000 is a valid normal carrier and decomposes exactly. 0x3f800001 fails TF32EncodingValid because a required low-zero bit is set.

When reading a consumer, check encoding validity before treating classification or decomposition fields as a usable finite value.

NDF clauses

Bodies come from owning ASL. Dragging or buttons change only this page-session view order.

No NDF clause is attached to this unit.

Evidence index

8 matching entries

Executable evidence2
  • PTO-ARCH-DATA-TYPES-FORMAT-TF32 compiles as an independent normative unit
    1. surfaceARCH
    2. ownerPTO-ARCH-DATA-TYPES-FORMAT-TF32
    3. categorySTATIC-INVARIANT
    4. case001
    Show exact test source
    Sources and references
    Complete stable ID
    PTO-AVS-ARCH-DATA-TYPES-FORMAT-TF32-STATIC-001
    Path
    tests/asl/arch/data-types/formats/tf32/arch-static-tf32-contract-001.asl
    Kind / role
    static-invariant
    Pass condition
    the complete model and this unit's static invariant compile
    SHA-256
    3a8f1ca2a3ce3a2582099aa5cfa8f295e7c4474b19e3e45c3f7298797db694c4
    Open exact source ↗ for PTO-AVS-ARCH-DATA-TYPES-FORMAT-TF32-STATIC-001
  • TF32 exposes its exact descriptor and finite-value decomposition.
    1. surfaceARCH
    2. ownerPTO-ARCH-DATA-TYPES-FORMAT-TF32
    3. categoryBOUNDARY
    4. case001
    Show exact test source
    Sources and references
    Complete stable ID
    PTO-AVS-ARCH-TF32-DECOMP-001
    Path
    tests/asl/arch/data-types/formats/tf32/arch-bound-tf32-decomp-001.asl
    Kind / role
    boundary
    Requirements
    PTO-NUMERIC-FINITE-DECOMPOSITION-001
    Pass condition
    Field metadata, finite boundaries, unavailable special values, and existing value-class rules agree.
    SHA-256
    2b011596bc0e6d292dcee10a65971c514db4d829beae9d0b438ac7cf098b9e57
    Open exact source ↗ for PTO-AVS-ARCH-TF32-DECOMP-001
Commit-scoped evidence5
  • spec/evidence/release-traceability-readiness.json · closedPTO-EVIDENCE-RELEASE-TRACEABILITY
    Sources and references
    Complete stable ID
    PTO-EVIDENCE-RELEASE-TRACEABILITY
    Path
    spec/evidence/release-traceability-readiness.json
    Kind / role
    ASL/NDF/documentation/AVS traceability
    SHA-256
    c7327021d39dc67ac5564bc55073b3870a397d79ac8d9648284d56e33bc14a3e
    Open exact source ↗ for PTO-EVIDENCE-RELEASE-TRACEABILITY
  • spec/evidence/instruction-contract-closure.json · closedPTO-EVIDENCE-INSTRUCTION-CONTRACT-CLOSURE
    Sources and references
    Complete stable ID
    PTO-EVIDENCE-INSTRUCTION-CONTRACT-CLOSURE
    Path
    spec/evidence/instruction-contract-closure.json
    Kind / role
    mnemonic and encoding contract closure
    SHA-256
    3ef2bb62421c79dff8fa77a1c7983923b523244b8090812883ef81286ca8106a
    Open exact source ↗ for PTO-EVIDENCE-INSTRUCTION-CONTRACT-CLOSURE
  • spec/evidence/architecture-readiness.json · openPTO-EVIDENCE-ARCHITECTURE-READINESS
    Sources and references
    Complete stable ID
    PTO-EVIDENCE-ARCHITECTURE-READINESS
    Path
    spec/evidence/architecture-readiness.json
    Kind / role
    architecture maturity and blockers
    SHA-256
    4b0b85199101251bea744e0f3591cc31906909dc80d5ab651c417a936036a004
    Open exact source ↗ for PTO-EVIDENCE-ARCHITECTURE-READINESS
  • spec/evidence/release-gate-readiness.json · ready-for-exact-head-verificationPTO-EVIDENCE-RELEASE-GATE-READINESS
    Sources and references
    Complete stable ID
    PTO-EVIDENCE-RELEASE-GATE-READINESS
    Path
    spec/evidence/release-gate-readiness.json
    Kind / role
    exact-head gate readiness
    SHA-256
    a0f4d2b6920c08981ea55fd8ef820708a40d4feb5402c5150e8e9ab532d84ce0
    Open exact source ↗ for PTO-EVIDENCE-RELEASE-GATE-READINESS
  • spec/release-manifest.json · draftPTO-EVIDENCE-RELEASE-MANIFEST
    Sources and references
    Complete stable ID
    PTO-EVIDENCE-RELEASE-MANIFEST
    Path
    spec/release-manifest.json
    Kind / role
    release content and encoding fingerprints
    SHA-256
    1a64c109ed7a90351c41e2a418b3c0ebaf8ad975838986d2101385186b85c0d8
    Open exact source ↗ for PTO-EVIDENCE-RELEASE-MANIFEST
Decision history1
  • Numeric format value classification · accepted
    1. decision recordADR
    2. case0048

    Decision record

    Loading ADR-0048…

    Sources and references
    Complete stable ID
    ADR-0048
    Path
    docs/status/decisions/0048-numeric-format-value-classification.md
    Affected units
    PTO-ARCH-DATA-TYPES-FORMAT-BF16, PTO-ARCH-DATA-TYPES-FORMAT-DESCRIPTOR, PTO-ARCH-DATA-TYPES-FORMAT-E1M2X2, PTO-ARCH-DATA-TYPES-FORMAT-E2M1X2, PTO-ARCH-DATA-TYPES-FORMAT-E2M3, PTO-ARCH-DATA-TYPES-FORMAT-E3M2, PTO-ARCH-DATA-TYPES-FORMAT-E4M3, PTO-ARCH-DATA-TYPES-FORMAT-E5M2, PTO-ARCH-DATA-TYPES-FORMAT-E8M0, PTO-ARCH-DATA-TYPES-FORMAT-FP16, PTO-ARCH-DATA-TYPES-FORMAT-FP32, PTO-ARCH-DATA-TYPES-FORMAT-FP64, PTO-ARCH-DATA-TYPES-FORMAT-HF32, PTO-ARCH-DATA-TYPES-FORMAT-HIF4X2, PTO-ARCH-DATA-TYPES-FORMAT-HIF8, PTO-ARCH-DATA-TYPES-FORMAT-TF32, PTO-ARCH-DATA-TYPES-NUMERIC-CLASSIFICATION, PTO-ARCH-DATA-TYPES-NUMERIC-FORMATS, PTO-SCALAR-FMAX, PTO-SCALAR-FMIN, PTO-SCALAR-MODEL-FSU-PROFILE, PTO-TILE-MODEL-EXECUTION-COMPARISON, PTO-TILE-MODEL-EXECUTION-FUSED-MULTIPLY-ADD, PTO-TILE-MODEL-EXECUTION-UNARY, PTO-TILE-MODEL-NUMERIC-FORMATS, PTO-TILE-MODEL-ORDERING-SORTING, PTO-TILE-TMAX, PTO-TILE-TMIN
    Affected NDF
    PTO-FMAX-DECISION-BINDING-001, PTO-FMIN-DECISION-BINDING-001, PTO-NUMERIC-FINITE-DECOMPOSITION-001, PTO-NUMERIC-FORMAT-DESCRIPTOR-001, PTO-TMAX-CONTRACT-001, PTO-TMIN-CONTRACT-001
    SHA-256
    ce3ecd1851e22b5517d07076ab8bd2db36b6b4582111c761db19240275853d9c
    Open exact decision source ↗ for ADR-0048

Unit metadata

Open 4 generated metadata fields
id
PTO-ARCH-DATA-TYPES-FORMAT-TF32
surface
arch
classification
[
  "data-types",
  "formats",
  "tf32"
]
depends_on
[
  "PTO-ARCH-DATA-TYPES-FORMAT-DESCRIPTOR"
]
Open generated traceability record
{
  "classification": [
    "data-types",
    "formats",
    "tf32"
  ],
  "documentation": "docs/arch/data-types/formats/tf32.md",
  "id": "PTO-ARCH-DATA-TYPES-FORMAT-TF32",
  "mnemonic": null,
  "readiness_subjects": [
    "ADR-0048"
  ],
  "semantic_tests": [
    "PTO-AVS-ARCH-TF32-DECOMP-001"
  ],
  "source": "asl/arch/data-types/formats/tf32.asl",
  "surface": "arch",
  "tests": [
    "PTO-AVS-ARCH-DATA-TYPES-FORMAT-TF32-STATIC-001",
    "PTO-AVS-ARCH-TF32-DECOMP-001"
  ]
}

Sources and release identity

Show commit, paths, hashes, version, and canonical owners
Release
0.58.5 · Release candidate
Commit
7dc8b7e5b121d2b2499a2273bebff29e2cd86812
ASL SHA-256
1b1a14d0d609cc41a312e59df8621a0f3ac711a8589c5e99844aa80fb0885873
Generated documentation
docs/arch/data-types/formats/tf32.md · embedded in this page
Documentation SHA-256
3bcef7d67e7430ed6d5b7632b4bfd50910a16eb320d78d95f2b01efe26d4f26e

Exact owners