docs/spec-fabric-switch.md

← all documents
not measured0highlighted source passages0/0PBTs with runs0draft PRs
Not estimatedcombined confidence estimate0 considered · 0 missing
How combined confidence is computed

max(0, 1 − sum of PBT residual-risk estimates). Uses each distinct available PBT’s latest-run estimate and its own sampling scope; PBTs without estimates are reported and omitted. An observed violation remains the suite result; when other PBTs have estimates, their estimate is still shown. Assumes no independence. This is a combined point estimate, not a statistical confidence bound or deployment reliability. Uncovered passages are outside its scope.

No PBTs registered for this file.

Code coverageNot measured

Coverage added over the baseline, grouped by PBT. Only files with gains appear below.

No added coverage recorded.

Files without added coverage and unmeasured PBTs
Source fileBaseline coverageBaseline + inputContributing input
–

docs/spec-fabric-switch.md · pinned revision 48615bc5925ef4b9db8b4550b5d4322933cf4b7b

1

Fabric Switch

3

This document specifies fabric.switch, the leaf-level routing op of the fabric dialect.

6

Identity

8
  • Mnemonic: switch.
  • Variadic SSA inputs and variadic SSA outputs (anonymous form) or a zero-operand / zero-result template (named form) whose port signature is captured in a function_type attribute.
  • Carries a mandatory Fabric_ScheduleAttr predicate [spatial] or [temporal] (reused from fabric.pe).
  • Optional sym_name so a switch can be referenced by fabric.instantiate (mirrors fabric.pe and fabric.fu).
  • The op has no body region; routing is fully described by attributes.
  • Allowed only inside a fabric.module body.
19

fabric.switch owns architecture capability: physical ports, allowed input-to-output traversals, bounded configured-entry capacity, and observable transfer, grant, and progress behavior. SpatialMapping owns selected traversals, Physical Tags at real writers or ingresses, event-relative use, and configured route semantics. A Mapping-selected exact hardware refinement may select among Fabric-declared cycle-observable alternatives. Finalization assigns semantic rows deterministically. ConfigurationABI alone owns their physical encoding; an implementation owns only the circuitry and microstate that implement the exact Fabric/Mapping contract.

29breadth-09 · sampled attempt

Schedule predicate and port types

The schedule predicate selects the port type kind of every input and output of the op. The two cases are mutually exclusive.

Schedule Port type Uniformity
spatial !fabric.bits<W> All ports must share the same W (>= 0).
temporal !fabric.bits_tag<W, T> All ports must share the same (W, T) (W >= 0, T >= 1).

Spatial ports may not use bits_tag; temporal ports may not use bits.

41

In both forms, K = numInputs() >= 1, L = numOutputs() >= 1, and K * L <= 256. For the named form K/L are taken from the function_type signature; for the anonymous form they are the SSA operand and result counts. The product check uses overflow-safe arithmetic.

46

Each fabric.switch denotes one physical crossbar. A switch with K * L > 64 remains valid through the hard 256-crosspoint limit, but verification emits a non-fatal implementation-efficiency warning. The warning is advisory output, does not enter Fabric identity, and does not change Mapping legality or resource capacity. Larger networks are expressed by composing switch occurrences with explicit Fabric connections, not by bypassing the limit with another routing primitive. Thus 9 x 1 is below the warning threshold, 8 x 9 warns, 16 x 16 warns but remains valid, and 17 x 16 is invalid.

56

This uniformity rule describes the switch's own declared physical ports. It does not require a neighboring producer or consumer to use the same width. A connection from a differently sized endpoint into a switch input, or from a switch output into a differently sized endpoint, uses the module-level LSB-aligned width rule in spec-fabric-module.md. That connection does not add an adapter and does not change the switch's internal crossbar width. Port-kind changes remain illegal without an explicit fabric.boundary.

65

For an anonymous switch, each incoming type-list entry may spell both endpoints as source-type to destination-port-type. The source type resolves the SSA operand; the destination type is the switch input-port type used by the uniformity and schedule checks. The clause accepts only bits to bits or bits_tag to bits_tag; widths normalize with the module-level LSB-aligned semantics. It rejects port-kind changes and memref. When to is absent, the destination type equals the source type. Named switch templates continue to derive all port types from their declared function_type signature.

75

Differing anonymous input-port types are retained in the ODS-owned typed inner_input_types : ArrayRef<Type> property. The custom assembly syntax renders that state through the per-input to clauses and leaves the property empty when every source and destination type is equal. A non-empty property has one entry per operand and must contain at least one actual endpoint-type difference.

82

Hardware parameters

84

Hardware parameters live in hw_params, an ArrayAttr of length 1 wrapping a DictionaryAttr (the same [ ... ] convention used by other fabric ops). fabric.switch requires hw_params to be present.

88
[{connectivity_table = ["0110", "1011", "1111"]}]                              // spatial
[{connectivity_table = ["0110", "1011", "1111"], route_table_size = 8 : i32,
  grant_policy = #fabric.switch_round_robin<requester_cycle = array<i64: 0, 1, 2, 3>, reset_requester = 0>}] // temporal
94

connectivity_table

96
  • ArrayAttr of L StringAttrs (one row per output).
  • Each row has length K (one character per input port).
  • Characters are exactly '0' or '1'.
  • Bit-string convention: MSB on the left. The leftmost character of a row corresponds to bit index K - 1 (the highest input port index); the rightmost character is bit index 0 (input port 0). This is the universal convention for bit-string attributes in the fabric dialect.
  • Per-row constraint: each row must contain at least one '1' (each output has at least one physical input source).
  • Per-column constraint: across the L rows, each column index (i.e., each input port) must contain at least one '1' in some row (each input has at least one physical destination).
109

route_table_size (temporal only)

111
  • IntegerAttr (i32), value >= 1.
  • Number of resident route-table entries the hardware allocates. It is an explicit bounded capacity, independent of 2^T, and does not allocate one row for every representable tag value.
  • Spatial switches MUST NOT carry route_table_size.
117breadth-02 · sampled attempt

grant_policy (temporal only)

The optional value is exactly one typed Fabric attribute:

#fabric.switch_fixed_priority<requester_order = array<i64: ...>>
#fabric.switch_round_robin<requester_cycle = array<i64: ...>,
                           reset_requester = ...>

Requester ordinals are the switch input-port ordinals. The sequence is a permutation of the complete input domain and contains no duplicate. The reset requester of a round-robin policy occurs in its cycle. A temporal switch whose physical connectivity admits two inputs to one output requires one exact policy in Fabric 1.0. A switch without such fan-in must omit it. Spatial switches must omit it.

134

Configured Mapping Projection

136

Configured parameters are a deterministic projection of SpatialMapping and are not part of the canonical hardware capability. The semantic projection is one closed sum:

140
SwitchConfiguration =
    Disabled
  | Active { route_table, physical_refinements }
146

Disabled carries no route table, tag, selector, or refinement. The physical enable bit and inactive encoding belong only to ConfigurationABI. An active projection whose route table selects no traversal canonicalizes to Disabled.

151

The bit strings in connectivity_table and route_table are canonical semantic representations of allowed and selected traversals. They are not a register layout or configuration-memory bit assignment. Only ConfigurationABI maps these semantic fields to physical encoding.

156

Canonical hardware-only Fabric has no selected configured projection. A finalized configured view must contain exactly one closed variant; mixing a raw enable field with an independently optional route table is invalid.

160

route_table -- spatial

162
  • ArrayAttr of L StringAttrs (one row per output).
  • Row j has length equal to the count of '1's in connectivity_table[j] (i.e., the number of physically-connected inputs for output j).
  • Bit-string convention: MSB on the left (same as connectivity_table).
  • Each row has AT MOST ONE '1' bit (zero '1's means the output is temporarily routed nowhere).
  • The position of the '1' selects which physically-connected input is routed to that output. Counting bit positions from the right (LSB-first) on the route_table row, position p selects the p-th '1' (also counted from the right, LSB-first) in the corresponding connectivity_table row.
176

Spatial switches allow broadcast (one input may be selected by multiple route_table rows simultaneously) but FORBID fan-in to a single output (the per-row '1' <= 1 rule enforces this).

180

At the enclosing fabric.module SSA level, broadcast does not reuse the input transport at multiple consumers. The switch consumes that input once and exposes each selected output port as a distinct SSA result. Each result remains a point-to-point transport under spec-fabric-module.md.

186

route_table -- temporal

188
  • ArrayAttr of exactly route_table_size entries.
  • Each entry is one closed typed variant:
  • Unused, with no fields; or
  • Active { route_sel, tag }.
  • Each Active entry has two fields:
  • route_sel -- ArrayAttr of L StringAttrs with the same shape as a spatial route_table.
  • tag -- IntegerAttr of width T (matching the port tag width), value in [0, 2^T).
  • Per-entry route_sel follows the spatial-route-table per-row rules (each row at most one '1').
  • Tag uniqueness. Among Active entries, all tag values must be distinct. Two Active entries sharing a tag value is a configuration error (it would cause runtime ambiguity when a token arrives carrying that tag). An all-Unused table canonicalizes to Disabled.
205

The table performs exact content match across Active resident entries. The tag does not directly index a 2^T-deep array, and route-table row identity is not a software stream identity. The configured tag is derived from Mapping-owned writer continuity and ResourceUse sharing assignments. It is a local interpretation key where co-resident incompatible routes require distinction, not a firing, iteration, invocation, or logical-token identity.

212

SpatialMapping derives one route segment at this switch as the exact signature

214
SwitchRouteSegment = (input, exact_output_set)
218

projects selected demands into resident rows. Physical Tag is part of the selected row demand: all demands with the same (switch occurrence, Physical Tag) name one resident row, while distinct tags necessarily name distinct rows. Same-tag demands are legal only when their signatures are compatible. Two signatures with the same input are compatible only when their exact output sets are equal. Signatures with different inputs are compatible only when their output sets are disjoint. These are the complete merge rules: subset, superset, or partially overlapping output sets do not merge. Consequently a resident row neither adds a crosspoint to any constituent demand nor creates an unrequested broadcast or fan-in.

229

The canonical exact projection groups by occurrence and numeric tag and orders rows by occurrence and unsigned tag. Its row count, rather than continuity- segment count, is the exact route_table_size consumption. During search only, Fabric also projects candidates with unassigned tags: assigned rows retain their exact identity, and each unassigned demand enters the first compatible assigned or provisional row, opening a tagless provisional row otherwise. That projection is a lower bound with no configuration identity; it cannot be published, configured, or executed. PnR capacity and route cost use its marginal row increase until tags are assigned. The strict verifier rebuilds the exact tagged projection and proves that every selected crosspoint belongs to at least one constituent signature and every constituent signature is represented exactly. An incompatible same-tag row remains explicit while PnR repairs its TagConflict; it can contribute physical handshake demand but cannot pass strict Mapping verification or become configuration.

244

Configuration field carrier

246

Each switch occurrence owns exactly one ordinal-zero FabricSemanticConfigFieldRef with one Fabric-owned direct-bit relation. Let C be the canonical concatenation, by output ordinal and then admitted input ordinal, of all physically admitted crosspoints. A Spatial switch carrier is exactly |C| bits. Bit one selects that crosspoint, every output group has at most one selected bit, broadcast across output groups is legal, and the all-zero carrier is Disabled.

254

For a Temporal switch, one resident entry contains one valid bit, T tag bits, and |C| route bits in that order. Entries concatenate by resident-entry ordinal. An invalid entry has every remaining bit zero. A valid entry obeys the same per-output route rule, selects at least one crosspoint, and valid entries have distinct tags. An all-invalid carrier is Disabled. Unused high bits in the final byte are zero under the shared bit-vector convention.

261

This carrier is the canonical semantic projection of the complete route table, not its SRAM address layout. ConfigurationABI may place its bits only through the one direct field; it cannot create per-output or per-entry fields whose independent values bypass route-table validation.

266

Configured-hardware projection consumes exact tagged rows from the Spatial switch-demand function, preserves membership established by the Fabric-owned route-signature compatibility predicate, orders active rows by unsigned tag, and fills the remaining rows with Unused. The Fabric codec validates the table bound, tag width and uniqueness, admitted crosspoints, exact signature preservation, and per-output fan-in before ConfigurationABI assigns a physical layout. Neither Mapping nor a backend stores an independent route-row selection or re-packs rows privately.

275

Handshake Dependency Projection

277

connectivity_table declares capability and contributes no active arc by itself. Absent an exact holding or registered refinement, each selected spatial row or resident temporal row derives both the input-valid to selected- output-valid dependency and the selected-output-ready to selected-input-ready dependency. A unicast traversal therefore propagates both halves of ready/valid flow. For atomic broadcast, every selected output-ready signal participates in the one selected input's readiness because the source cannot retire until every selected sink accepts. A Fabric-declared temporal grant, holding, or registered refinement owns its replacement arc set and any stateful break; it cannot silently retain or remove the zero-state arcs.

288

For one selected input with valid signal v, selected output set S, and output-ready signals r[i], the stateless atomic broadcast equations are:

291
input_ready       = AND(r[j] for j in S)
output_valid[i]   = v AND AND(r[j] for j in S where j != i)
fire              = v AND AND(r[j] for j in S)
297

The peer-ready term prevents one output from accepting before all other selected outputs are ready. A direct dependency projection contains a quadratic boundary relation for a large broadcast. The sealed Fabric owner model may instead use canonical prefix and suffix conjunction junctions, or a smaller direct form for low fanout, provided each exact selection preserves the same boundary dependency reachability and atomic firing behavior. Junctions are private derived nodes; they are not switch ports, configuration entries, or Mapping-visible resources. Fabric does not enumerate destination subsets.

306

Disabled outputs, Unused temporal entries, and connectivity alternatives not selected by the configured route table contribute no arc. All resident Active temporal entries contribute their possible arcs even though runtime tags choose which entry handles a token; a trace-specific tag value cannot erase a structural dependency. These projections feed the two gates in docs/spec-fabric-module.md and docs/spec-mapping-verification.md and are not stored as a second switch graph.

314

Tag-driven trigger semantics

316

When a token arrives at an input port carrying tag value t, the switch looks up the unique Active route_table entry whose tag == t and uses that entry's route_sel as the spatial-style routing for the cycle's tokens carrying tag t. Different tags routed in the same cycle share the physical crossbar; same-cycle conflicts on a single output port (multi-input-to-same-output across different tags) request a grant under the switch's exact Fabric-owned GrantPolicy or a Mapping-selected exact hardware refinement declared by Fabric. The implementation executes that policy; it does not choose one.

326

Hardware payload opacity

328

A switch routes physical valid/ready transfers and treats the payload bits as opaque. It does not assign or interpret software-level value, control, or completion semantics.

332

Transfer Guarantees And Arbitration

334

The architecture-level routing rules are:

336
  • Spatial: broadcast (single input -> multiple outputs) is allowed; fan-in (multiple inputs -> single output) is FORBIDDEN. The verifier enforces fan-in rejection via the per-row '1' <= 1 rule on route_table.
  • Temporal: broadcast and time-multiplexed fan-in are allowed; multi-input-to-same-output requests across different tags compete for the declared output capacity.
344

Temporal fan-in never means combinational merging. Each Active row still selects at most one input per output. Competing rows share a physical resource over time. Fabric owns request eligibility, output capacity, exact grant and state-update behavior, latency, and backpressure visibility. The shared FixedPriority and RoundRobin semantics are owned by docs/spec-fabric-resource-contract.md. This switch schema owns its exact schedule-specific requester inventory, typed attribute syntax, ResourceState values, canonical initial state, capacity dimensions, stable typed requester order, and atomic transfer UsePatterns.

354

Its normalized resource projection is linear in physical connectivity:

356
  • every input and output port owns one unit-capacity service state;
  • every admitted (input, output) traversal owns one UsePattern that claims those two service states at one atomic transfer event;
  • every spatial traversal belongs to the switch's one static-configuration requester; and
  • temporal patterns sourced by one input share that input's requester.
363

The schedule determines when those service claims constrain Mapping. Spatial traversals are resident selections, so their implied claims participate in static route capacity closure. Temporal traversal patterns instead describe runtime service eligibility: different resident tag rows may select the same physical input or output, and same-cycle demand is resolved by the declared GrantPolicy. Static Mapping capacity therefore does not sum every resident Temporal row as simultaneous port occupancy. The independent resident limit is route_table_size, and exceeding it is CapacityOveruse.

372

For a spatial switch, Mapping selects the exact active traversal set before execution. Its capacity closure forbids two selected inputs from consuming the same output state, so physical fan-in alternatives do not imply a runtime arbiter or GrantPolicy. Different logical transfers remain different Mapping uses even though their alternative patterns share the one configuration requester. A temporal switch can make several input requesters eligible at runtime and therefore owns the exact GrantPolicy required by such fan-in.

380

For one selected broadcast, traversal uses with the same Mapping-derived activation, trigger, and concrete logical parameters form the exact atomic activation set defined by docs/spec-pnr.md. A Spatial switch groups selected outputs by (switch occurrence, input): outputs selected from one input commit as one broadcast, while different inputs remain different activations even though every Spatial traversal shares the switch's static-configuration requester. A Temporal switch instead groups by (configured row, input), so another resident tag row at the same input is a different activation. Repeated claims on one activation's shared ingress normalize to one physical claim. The source cannot retire until its exact output set acquires and commits, so no egress can be granted independently. In both schedules the Fabric requester group owns resource arbitration or configuration; it never merges Mapping-derived execution activations. Fabric does not enumerate the power set of possible broadcast destinations.

395

Fabric 1.0 requires an exact policy whenever temporal physical connectivity admits fan-in between runtime requesters. A later exact Fabric-owned refinement domain may broaden that authoring surface, but Mapping, simulation, runtime, and RTL lowering may not fill in a missing policy or choose a default. Cursor and reservation state are nonpersistent execution state. The implementation owns the arbiter circuit and transient cursor, but not the cycle-visible policy semantics. Spatial fan-in alternatives remain statically capacity-closed and must not manufacture either an arbiter or a policy.

404

Broadcast backpressure contract

406

A selected single-input/multi-output transfer is one atomic message replication. The source retires only when every selected sink accepts, or when the implementation first commits the complete replication into explicit holding state. Partial delivery, duplicate delivery, hidden draining, and reordering are invalid. The equations in Handshake Dependency Projection are the stateless architecture contract. A compact equivalent dependency graph is an implementation projection of those equations and must not become an additional architecture or Mapping authority.

415

Assembly format

417

Anonymous spatial:

419
%o:3 = fabric.switch [spatial] %i0, %i1, %i2, %i3
       [{connectivity_table = ["0110", "1011", "1111"]}]
       : (!fabric.bits<32>, !fabric.bits<32>, !fabric.bits<32>, !fabric.bits<32>)
      -> (!fabric.bits<32>, !fabric.bits<32>, !fabric.bits<32>)
426

Anonymous temporal:

428
%o:3 = fabric.switch [temporal] %i0, %i1, %i2, %i3
       [{connectivity_table = ["0110", "1011", "1111"],
         route_table_size = 8 : i32,
         grant_policy = #fabric.switch_round_robin<requester_cycle = array<i64: 0, 1, 2, 3>, reset_requester = 0>}]
       : (!fabric.bits_tag<32, 4>, !fabric.bits_tag<32, 4>, !fabric.bits_tag<32, 4>, !fabric.bits_tag<32, 4>)
      -> (!fabric.bits_tag<32, 4>, !fabric.bits_tag<32, 4>, !fabric.bits_tag<32, 4>)
437

The corresponding configured projections are represented semantically as:

439
Active {
  route_table = ["01", "100", "0100"]
}

Active {
  route_table = [
    Active { route_sel = ["01", "100", "0100"], tag = 10 },
    Active { route_sel = ["10", "001", "0001"], tag = 11 },
    Unused, ...
  ]
}
453

Named hardware template (spatial):

455
fabric.switch @MySw [spatial]
       (!fabric.bits<32>, !fabric.bits<32>) -> (!fabric.bits<32>, !fabric.bits<32>)
       [{connectivity_table = ["11", "11"]}]
461

Named hardware template (temporal):

463
fabric.switch @MySwT [temporal]
       (!fabric.bits_tag<32, 4>, !fabric.bits_tag<32, 4>)
        -> (!fabric.bits_tag<32, 4>, !fabric.bits_tag<32, 4>)
       [{connectivity_table = ["11", "11"], route_table_size = 1 : i32,
         grant_policy = #fabric.switch_fixed_priority<requester_order = array<i64: 0, 1>>}]
471

Hardware-only forms have no selected configured projection. Configured examples illustrate the derived Mapping projection; they do not make sw_configs part of Fabric hardware identity.

475

Reusable named templates are hardware-only. A configured projection belongs to a concrete elaborated occurrence's derived configured view and may not be stored on the template as shared workload state. Its HardwareConfigurationImage encoding is produced only through the exact ConfigurationABI.

481

Verifier rules

483
  • K >= 1, L >= 1, and the overflow-safe product K * L <= 256.
  • K * L > 64 emits the non-fatal large-crossbar warning exactly once for that switch verification; it does not make an otherwise valid switch invalid through 256 crosspoints.
  • Schedule + port type-kind correspondence (spatial -> bits, temporal -> bits_tag); uniform W (and T for temporal).
  • hw_params shape: length-1 ArrayAttr wrapping a DictionaryAttr.
  • connectivity_table: length L, each row length K, only '0'/'1', per-row >= 1 '1', per-column >= 1 '1'.
  • Spatial: route_table_size MUST NOT be present.
  • Temporal: route_table_size MUST be present and >= 1.
  • Spatial: grant_policy MUST NOT be present.
  • Temporal: an authored typed grant_policy has a non-empty, duplicate-free requester sequence, and a round-robin reset requester is in the cycle. Root-complete Fabric finalization requires exactly one policy for physical fan-in, forbids one without fan-in, and validates that its sequence is a permutation of every input ordinal.
  • A configured occurrence is exactly Disabled or Active; the inactive variant carries no route fields.
  • Active: route_table shape and per-row constraints, with an all-Unused table canonicalized to Disabled.
  • Spatial: route_table per-row '1' count <= 1.
  • Temporal: route_table length equals route_table_size; per-entry route_sel follows the spatial-row rules; tag integer width equals T; among Active entries tag values are distinct.
  • Named form has zero SSA operands and zero SSA results; signature lives in function_type, and reusable templates do not carry sw_configs. Anonymous form has variadic SSA operands and variadic SSA results and must NOT carry function_type.
513

Cross-references

515
  • spec-fabric-module.md -- top-level module body whitelist (which lists fabric.switch alongside fabric.pe, fabric.fifo, fabric.boundary, etc.).
  • spec-fabric-pe.md -- schedule predicate (spatial / temporal) shared with fabric.switch.
  • spec-fabric-system-adg.md -- Transport Architecture capacity and guarantee ownership versus concrete Interconnect Implementation state.