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.
Coverage added over the baseline, grouped by PBT. Only files with gains appear below.
No added coverage recorded.
| Source file | Baseline coverage | Baseline + input | Contributing input |
|---|
This document specifies fabric.switch, the leaf-level routing op of the
fabric dialect.
switch.function_type attribute.Fabric_ScheduleAttr predicate [spatial] or
[temporal] (reused from fabric.pe).sym_name so a switch can be referenced by
fabric.instantiate (mirrors fabric.pe and fabric.fu).fabric.module body.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.
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.
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.
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.
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.
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.
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.
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.
[{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
L StringAttrs (one row per output).K (one character per input port).'0' or '1'.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.'1' (each
output has at least one physical input source).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).IntegerAttr (i32), value >= 1.2^T, and does not allocate one
row for every representable tag value.route_table_size.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.
Configured parameters are a deterministic projection of SpatialMapping and are not part of the canonical hardware capability. The semantic projection is one closed sum:
SwitchConfiguration =
Disabled
| Active { route_table, physical_refinements }
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.
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.
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.
L StringAttrs (one row per output).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).connectivity_table).'1' bit (zero '1's means the output is
temporarily routed nowhere).'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.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).
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.
route_table_size entries.Unused, with no fields; orActive { route_sel, tag }.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).route_sel follows the spatial-route-table per-row rules
(each row at most one '1').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.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.
SpatialMapping derives one route segment at this switch as the exact signature
SwitchRouteSegment = (input, exact_output_set)
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.
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.
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.
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.
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.
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.
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.
For one selected input with valid signal v, selected output set S, and
output-ready signals r[i], the stateless atomic broadcast equations are:
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)
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.
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.
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.
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.
The architecture-level routing rules are:
'1' <= 1 rule on
route_table.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.
Its normalized resource projection is linear in physical connectivity:
(input, output) traversal owns one UsePattern that claims
those two service states at one atomic transfer event;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.
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.
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.
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.
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.
Anonymous spatial:
%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>)
Anonymous temporal:
%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>)
The corresponding configured projections are represented semantically as:
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, ...
]
}
Named hardware template (spatial):
fabric.switch @MySw [spatial]
(!fabric.bits<32>, !fabric.bits<32>) -> (!fabric.bits<32>, !fabric.bits<32>)
[{connectivity_table = ["11", "11"]}]
Named hardware template (temporal):
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>>}]
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.
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.
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.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'.route_table_size MUST NOT be present.route_table_size MUST be present and >= 1.grant_policy MUST NOT be present.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.Disabled or Active; the inactive
variant carries no route fields.route_table shape and per-row constraints, with an all-Unused
table canonicalized to Disabled.route_table per-row '1' count <= 1.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.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.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.