Skip to content
Public template

About

Formal Definition of PTO Instruction Set Architecture

Topics

Resources

Code of conduct

Contributing

Security policy

Stars

7 stars

Watchers

0 watching

Forks

PTO ISA Formal Specification

PR checks Exact-head release verification PTO ISA releases License: BSD 3-Clause

pto-spec is the executable ASL1 specification of the PTO Instruction Set Architecture. It defines a 64-bit scalar ISA, bundle and command forms, direct Tile operations, architectural state, legality, faults, completion, and memory ordering in one reviewable model.

The working tree is a normative draft and may contain architecture changes for a future release. Published versions are listed in GitHub Releases. Each release identity binds one commit and its reproducible formal evidence; downstream consumers pin that identity instead of following the moving development branch.

PTO ISA at a glance

Working-tree identity: architecture 0.58.7, publication candidate 0.58.7.0. This development inventory is generated from the live catalogs and ASL owners; it does not establish publication or release readiness.

Surface Current executable inventory
Scalar instruction forms 467
Active bundle and command forms 96
Direct Tile operations 119
Architecture and instruction ASL units 919

The generated release-traceability view contains the complete ASL-to-documentation-to-AVS inventory for the current tree.

Architecture scope

PTO ISA specifies:

  • a 64-bit scalar execution surface covering address generation, integer and logical operations, atomics, branches, floating-point support, and system operations;
  • a 32-code scalar register namespace with 24 absolute GPRs and T/U temporary queues, plus predicate state and an independent execution mask;
  • bundle-visible program-control, argument, dimension, data-attribute, ordering-attribute, IO-binding, and completion state;
  • 64 flat T/U/M/N Tile registers with explicit Local and Shared ownership, allocation, descriptors, valid regions, and definedness;
  • direct Tile operations for elementwise computation, reductions and expands, memory and data movement, matrix and matrix-vector work, layout changes, and irregular operations;
  • exact instruction masks, fields, constraints, selector values, decoder witnesses, and architectural effects;
  • explicit legality and fault ordering before effects, including aliasing, rollback, restart, and instruction-granular memory completion;
  • explicit compatibility declarations for behavior that is not portable across implementations.

Hardware pipelines, physical Tile allocation, backend intrinsics, latency, throughput, and target scheduling are outside the portable PTO ISA contract.

Instruction families

Family What it defines Reference
Architecture Public types, state, memory model, traps, and classification docs/arch/
Block BSTART, BSTOP, bundle configuration, bindings, and block execution docs/block/
Scalar AGU, ALU, AMO, BRU, FSU, SYS, compressed, half-long, and long forms docs/scalar/
Tile Direct Tile operations and their execution contracts docs/tile/

The B prefix denotes a bundle instruction. BLOCKNUM, BLOCKID, and CROSS_BID instead describe virtual core-block topology. These concepts share spelling history but represent different architectural state.

Start reading

Start with the architecture overview, then use the instruction classification to understand the current Tile classes and execution engines. The block, scalar, and Tile references above contain generated ASL mirrors and bounded supplementary explanation.

Machine-readable accepted forms and selectors live under spec/catalog/. Current architecture gaps are listed under docs/status/open/, while accepted decision history is kept under docs/status/decisions/. Release identities and evidence entry points are collected in the release hub.

Quick start

The lightweight development path needs Git, GNU Make, and Python 3.11 or newer:

git clone --recurse-submodules https://github.com/PTO-ISA/pto-spec.git
cd pto-spec
make pr-check

See Getting started for environment setup, the full formal-validation prerequisites (which add OCaml/opam, the pinned ASLRef fork, and the Rust toolchain for the NDF parity check), and troubleshooting. The repository layout maps each source, generated projection, and executable evidence surface to its owner.

Project policy

Current architectural meaning has one source chain:

ASL/NDF owner -> generated Markdown mirror -> AVS -> commit-scoped evidence

ADRs record why an architectural choice was accepted, rejected, or superseded; they do not redefine current ISA behavior. The ADR process describes that boundary. Contributor commands and exact-commit release rules are documented in Validation, not duplicated on this landing page.

Read Contributing before changing ASL, tests, generators, or documentation. The project uses the BSD 3-Clause License; permitted external evidence and attribution are recorded in NOTICE.

About

Formal Definition of PTO Instruction Set Architecture

Topics

Resources

Code of conduct

Contributing

Security policy

Stars

7 stars

Watchers

0 watching

Forks

Releases

Packages

Used by

Contributors

Languages