Skip to main content

PTO-ARCH-DATA-TYPES-FORMAT-BF16

PTO-ARCH-DATA-TYPES-FORMAT-BF16

ASL pseudocode

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

// PTO-REQ-HARDWARE-NUMERIC-001: exact BF16 encoding and finite values.
pure func BF16NumericFormatDescriptor() => NumericFormatDescriptorbegin    return NumericFormatDescriptor {        available = TRUE, kind = NumericFormatKind_FixedBinary,        carrier_bits = 16, lane_bits = 16, lanes_per_carrier = 1,        sign_bits = 1, sign_bit = 15,        exponent_bits_min = 8, exponent_bits_max = 8,        fraction_bits_min = 7, fraction_bits_max = 7,        exponent_bias_available = TRUE, exponent_bias = 127,        required_low_zero_bits = 0, 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 BF16FiniteDecomposition(value: bits(16))    => (boolean, boolean, Word, integer {-1074..1023})begin    let exponent = value[14:7];    let fraction = value[6:0];    if exponent == Ones{8} then        return (FALSE, FALSE, Zeros{PTO_XLEN}, 0);    elsif exponent == Zeros{8} then        if fraction == Zeros{7} then            return (TRUE, value[15] == '1', Zeros{PTO_XLEN}, 0);        else return (TRUE, value[15] == '1',                     ZeroExtend{PTO_XLEN}(fraction), -133);        end;    else return (TRUE, value[15] == '1',                 LSL(Zeros{PTO_XLEN} + 1, 7) +                     ZeroExtend{PTO_XLEN}(fraction),                 (UInt(exponent) - (127 + 7))                     as integer {-1074..1023});    end;end;pure func ClassifyBF16(value: bits(16)) => NumericValueClassbegin    let exponent = value[14:7];    let fraction = value[6:0];    if exponent == Ones{8} then        if fraction == Zeros{7} then            if value[15] == '1' then return NumericValue_NegativeInfinity;            else return NumericValue_PositiveInfinity;            end;        elsif fraction[6] == '1' then return NumericValue_QuietNaN;        else return NumericValue_SignalingNaN;        end;    end;    return NumericValueClassFromFiniteSign(value[15],        exponent == Zeros{8} && fraction == Zeros{7},        exponent == Zeros{8} && fraction != Zeros{7});end;
pure func BF16CanonicalNaN() => Wordbegin    return Zeros{PTO_XLEN} + 0x7fc0;end;
pure func BF16SignedZeroEncodings() => (Word, Word)begin    return (Zeros{PTO_XLEN}, Zeros{PTO_XLEN} + 0x8000);end;
View the complete ASL owner
// PTO-UNIT: {"id":"PTO-ARCH-DATA-TYPES-FORMAT-BF16","surface":"arch","classification":["data-types","formats","bf16"],"depends_on":["PTO-ARCH-DATA-TYPES-FORMAT-DESCRIPTOR"]}// DOC-BEGIN: operation// PTO-REQ-HARDWARE-NUMERIC-001: exact BF16 encoding and finite values.
pure func BF16NumericFormatDescriptor() => NumericFormatDescriptorbegin    return NumericFormatDescriptor {        available = TRUE, kind = NumericFormatKind_FixedBinary,        carrier_bits = 16, lane_bits = 16, lanes_per_carrier = 1,        sign_bits = 1, sign_bit = 15,        exponent_bits_min = 8, exponent_bits_max = 8,        fraction_bits_min = 7, fraction_bits_max = 7,        exponent_bias_available = TRUE, exponent_bias = 127,        required_low_zero_bits = 0, 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 BF16FiniteDecomposition(value: bits(16))    => (boolean, boolean, Word, integer {-1074..1023})begin    let exponent = value[14:7];    let fraction = value[6:0];    if exponent == Ones{8} then        return (FALSE, FALSE, Zeros{PTO_XLEN}, 0);    elsif exponent == Zeros{8} then        if fraction == Zeros{7} then            return (TRUE, value[15] == '1', Zeros{PTO_XLEN}, 0);        else return (TRUE, value[15] == '1',                     ZeroExtend{PTO_XLEN}(fraction), -133);        end;    else return (TRUE, value[15] == '1',                 LSL(Zeros{PTO_XLEN} + 1, 7) +                     ZeroExtend{PTO_XLEN}(fraction),                 (UInt(exponent) - (127 + 7))                     as integer {-1074..1023});    end;end;pure func ClassifyBF16(value: bits(16)) => NumericValueClassbegin    let exponent = value[14:7];    let fraction = value[6:0];    if exponent == Ones{8} then        if fraction == Zeros{7} then            if value[15] == '1' then return NumericValue_NegativeInfinity;            else return NumericValue_PositiveInfinity;            end;        elsif fraction[6] == '1' then return NumericValue_QuietNaN;        else return NumericValue_SignalingNaN;        end;    end;    return NumericValueClassFromFiniteSign(value[15],        exponent == Zeros{8} && fraction == Zeros{7},        exponent == Zeros{8} && fraction != Zeros{7});end;
pure func BF16CanonicalNaN() => Wordbegin    return Zeros{PTO_XLEN} + 0x7fc0;end;
pure func BF16SignedZeroEncodings() => (Word, Word)begin    return (Zeros{PTO_XLEN}, Zeros{PTO_XLEN} + 0x8000);end;// DOC-END: operation

Architecture behavior

purpose scope

Purpose and scope

BF16 is an assigned PTO numeric format. This page helps a reader connect its carrier layout, finite-value decomposition, and value classification; the exact contract remains in BF16NumericFormatDescriptor, BF16FiniteDecomposition, and ClassifyBF16 in the ASL owner.

concepts state

Carrier and fields

The descriptor uses a 16-bit carrier, a 16-bit logical lane, and 1 lane(s) per carrier. The lane has one sign bit at position 15, 8 exponent bit(s), 7 fraction bit(s), and exponent bias 127.

No carrier bits are constrained outside the sign, exponent, and fraction fields.

rules interactions

Decomposition and classification

BF16FiniteDecomposition reports whether a finite decomposition is available and, when available, returns the sign, an integer significand, and a binary exponent. ClassifyBF16 separately assigns the raw lane to zero, subnormal, normal, infinity, or NaN classes supported by this format.

It has signed zero, subnormals, infinities, quiet NaNs, and signaling NaNs. An all-one exponent is not a finite decomposition; a zero fraction selects infinity and a nonzero fraction selects a NaN class.

boundaries

Boundaries and exact encodings

0x0000 and 0x8000 are the positive and negative zero encodings; 0x7fc0 is the canonical quiet NaN.

The finite-decomposition function reports availability with its returned tuple; value classification is a separate function result.

example usage

illustrative reading example

This example illustrates how to read the functions; it does not add an encoding rule.

For example, 0x0001 decomposes to a positive significand of 1 with exponent -133, while 0x7f80 is classified as positive infinity and has no finite decomposition.

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
  • BF16 exposes its exact descriptor and finite-value decomposition.
    1. surfaceARCH
    2. ownerPTO-ARCH-DATA-TYPES-FORMAT-BF16
    3. categoryBOUNDARY
    4. case001
    Show exact test source
    Sources and references
    Complete stable ID
    PTO-AVS-ARCH-BF16-DECOMP-001
    Path
    tests/asl/arch/data-types/formats/bf16/arch-bound-bf16-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
    0365cd116d6e360bc1dea6039b3adab8593befce550a249064f8d8bbb4d15892
    Open exact source ↗ for PTO-AVS-ARCH-BF16-DECOMP-001
  • PTO-ARCH-DATA-TYPES-FORMAT-BF16 compiles as an independent normative unit
    1. surfaceARCH
    2. ownerPTO-ARCH-DATA-TYPES-FORMAT-BF16
    3. categorySTATIC-INVARIANT
    4. case001
    Show exact test source
    Sources and references
    Complete stable ID
    PTO-AVS-ARCH-DATA-TYPES-FORMAT-BF16-STATIC-001
    Path
    tests/asl/arch/data-types/formats/bf16/arch-static-bf16-contract-001.asl
    Kind / role
    static-invariant
    Pass condition
    the complete model and this unit's static invariant compile
    SHA-256
    c4f3367ae73298b1e0c3cc6b865876f045ac3c63c4c83cb8a45f4b48152e2692
    Open exact source ↗ for PTO-AVS-ARCH-DATA-TYPES-FORMAT-BF16-STATIC-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-BF16
surface
arch
classification
[
  "data-types",
  "formats",
  "bf16"
]
depends_on
[
  "PTO-ARCH-DATA-TYPES-FORMAT-DESCRIPTOR"
]
Open generated traceability record
{
  "classification": [
    "data-types",
    "formats",
    "bf16"
  ],
  "documentation": "docs/arch/data-types/formats/bf16.md",
  "id": "PTO-ARCH-DATA-TYPES-FORMAT-BF16",
  "mnemonic": null,
  "readiness_subjects": [
    "ADR-0048"
  ],
  "semantic_tests": [
    "PTO-AVS-ARCH-BF16-DECOMP-001"
  ],
  "source": "asl/arch/data-types/formats/bf16.asl",
  "surface": "arch",
  "tests": [
    "PTO-AVS-ARCH-BF16-DECOMP-001",
    "PTO-AVS-ARCH-DATA-TYPES-FORMAT-BF16-STATIC-001"
  ]
}

Sources and release identity

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

Exact owners