Agentic System Design Automation for Tensor Computing

Introduction

For decades, computer systems were designed primarily for general-purpose applications, whose programs are expressed as control-flow-oriented computations and executed through instruction-set architectures. To manage the resulting optimization and verification complexity, human experts used domain knowledge to divide the system into layers, each with its own representation, constraints, and decision variables. This structure makes design-space exploration tractable because domain-specific optimization methods can focus on smaller, tightly coupled subsets of decisions, while interfaces limit the effects of choices across layers. It also makes verification tractable because correctness obligations can be stated and checked against well-defined layer contracts rather than against the full software–hardware system at once.

Modern AI and machine-learning systems increasingly rely on tensor computing. Their design now faces two simultaneous changes that create an opportunity for cross-layer co-design across software and hardware. First, agentic AI combines the semantic and reasoning capabilities of large language models with stochastic optimization methods—including reinforcement learning, Bayesian optimization, and evolutionary search—and can explore much larger, heterogeneous design spaces spanning software and hardware choices. Second, tensor computing differs fundamentally from control-intensive instruction execution: much of its computation, dependence, data movement, and resource use can be expressed before runtime, while a smaller residual set remains dynamic. Together, these developments may enable a new design paradigm for tensor-computing systems: end-to-end cross-layer optimization across the software–hardware stack.

The program is organized around three linked research questions:

1. End-to-end modeling. How can we construct a modeling framework that represents the design space from AI workload semantics through software, compilation, runtime, hardware architecture, and silicon-manufacturing technology, while supporting both optimization and verification?

2. Agentic exploration. How can we build an agentic optimization system that learns the internal structure of this heterogeneous design space, identifies important couplings and performance bottlenecks, and improves its exploration strategy over time?

3. Layered verification. How can we partition and connect verification across hardware design and fabrication, software and compilation-time mapping, and runtime adaptation, so each stage provides the required assurance within its available time and information?

Together, these questions define one program: the model exposes the design space, the agentic system explores it, and layered verification makes the resulting designs safe to adopt.

1. The Tractability Hypothesis and Its Limits

1.1 Two Sources of Design Complexity

Cross-layer design presents two different complexity problems. Optimization complexity is the cost of finding useful realizations among decisions whose effects may cross software, architecture, and physical implementation. It depends not only on the number of choices, but on how densely they interact, when their consequences become observable, and which choices have already been committed. Verification complexity is the cost of establishing that an admitted realization preserves the intended computation, respects finite resources, and remains correct over its allowed executions. The two are related but not identical. The tractability hypothesis therefore requires a separate factorization of each: design choices must have enough structure to guide search, and correctness obligations must have enough structure to be checked without treating every candidate or every payload history as one monolithic state space.

1.2 The Layered Bargain

Layering is the traditional bargain for controlling both. Each layer preserves a domain-specific structure—algebra and dependence in a compiler representation, transactions and ordering in a behavioral model, cycle-level causality in RTL, or placement, timing, power, and wiring in physical design. Local optimization can then focus on a smaller set of decisions, and local verification can rely on a narrower contract. The same interface becomes an optimization wall, however, when it hides a consequential choice, cost, or proof assumption. A compiler cannot account for a banking or routing interaction it cannot represent; a lower implementation can invalidate an upper proof when the assumption it must preserve was never exported. Removing the layers does not solve this problem: it discards useful inductive structure and replaces several bounded problems with one untyped, densely coupled space. A viable cross-layer approach must instead preserve layer-native structure while exposing every dependency, cost, and proof assumption that can change a decision elsewhere.

1.3 Tensor Structure and Its Preconditions

Tensor computing may make such exposure possible, but not merely because a program contains tensors or is drawn as dataflow. The relevant regions expose stronger structure: operations and numerical observations are declared; multidimensional iteration domains and producer–consumer relations are explicit; shapes, active index sets, or their bounds are fixed or parameterized at a region boundary; dependencies, data rates, addresses, and memory effects are regular or conservatively summarized; and computation, storage, communication, and allowed runtime variation are finite. Fixed-rate dataflow and affine program models show how some scheduling, dependence, and buffer questions can be reduced to structured relations rather than recovered from arbitrary execution histories [R10, R13]. These conditions do not prove tractability; they expose the stable facts on which the two factorizations could be built.

1.4 Optimization Tractability and Agentic Exploration

On the optimization side, explicit operations, geometry, dependencies, and resource effects turn fusion, layout, tiling, placement, buffering, routing, replication, recomputation, and pipeline organization into named decisions rather than hidden consequences of lowering. Their scopes and effects define a coupling structure. If most couplings concentrate within smaller groups and the remaining cross-effects can be bounded, the global space may decompose into tightly interacting subspaces. This does not reduce the raw number of combinations; it gives search a structure it can exploit and allows choices to be committed when the required information becomes available. The factorization fails when important interactions appear only after lowering, when physical effects such as placement-dependent timing, congestion, power delivery, temperature, process variation, test, or yield remain hidden, or when visible couplings stay dense across the software–hardware stack.

Agentic methods may exploit this optimization structure. They can propose and backtrack over cross-layer moves, learn which variables interact, accumulate evidence about bottlenecks, and direct evaluation toward promising regions. They cannot create a missing decision variable, recover a proof premise erased by an interface, make a densely coupled space sparse, or turn an illegal candidate into a correct implementation. Representation adequacy and search efficiency are separate questions; model-based constraints and checks, not the search agent, remain the authority for acceptance.

1.5 Verification Tractability and Its Limits

On the verification side, fixed or bounded geometry and payload-independent execution effects may permit reasoning over operation semantics, rates, dependence, resource bounds, and declared variation instead of enumerating payload-scale histories. Obligations over these facts can be reused across repeated tensor instances, while a concrete realization leaves a smaller residual set of dynamic behavior to check. TrainVerify provides narrow supporting evidence that shape reduction can make one class of distributed-training plan equivalence checks scale more slowly than tensor size [R25]. The causal claim remains conditional: payload may be abstracted only when it cannot change control, addressing, allocation, routing, synchronization, termination, or the observation being proved.

This verification factorization breaks when payload-dependent expert routing, filtering, sparse indices, or early termination turns shape and work count into runtime state; dynamic-network and mixture-of-experts systems expose this problem directly [R20, R27]. Irregular memory effects, unbounded queues or geometry, unconstrained faults, and value-dependent synchronization can likewise prevent compact summaries or reusable obligations. In these cases, tensor notation has not removed the relevant state; it has only hidden it.

1.6 Commitment Stages and Residual Runtime Freedom

The two factorizations are synthesized by distinguishing four spaces. The candidate space contains every realization the representation can construct and determines the optimization problem. The accepted, or certified, space contains only candidates that satisfy the required semantic, dependency, resource, and implementation conditions. The deployed space contains the accepted realizations actually bound to a target and workload context. The runtime space contains only the actions and states still permitted inside a deployed realization. Unselected hardware organizations, discarded mappings, and failed candidates belong to design exploration; they are not runtime behaviors that verification must enumerate. Search space is therefore not runtime state space, although either can remain large when the required factorization fails.

1.7 The Conditional Tractability Hypothesis

The tractability hypothesis is conditional and falsifiable. It holds only to the extent that consequential choices can be exposed before commitment, their interactions admit useful decomposition, accepted realizations can be checked through bounded obligations, and the remaining runtime freedom can be represented by a compact state and action space. It is not a claim that all tensor systems are static or easy. It is the narrower claim that a sufficiently structured region of tensor computation may support more cross-layer optimization without forcing optimization search and runtime verification into one monolithic problem. End-to-End Modeling therefore bears a concrete burden: preserve the useful structure of each layer while representing the cross-layer choices, couplings, commitments, and proof assumptions needed to make both factorizations real.

2. End-to-End Modeling

The purpose of the end-to-end model is to represent the cross-layer design space so optimization can reason over feasible, structured alternatives and correctness conditions can be preserved and checked as a tensor workload is transformed into a physical implementation. The represented object therefore spans tensor semantics, software transformations, compilation and mapping, runtime behavior, hardware architecture, physical implementation, and the semiconductor constraints that bound implementation and operation.

The difficulty is to gain this cross-layer visibility without losing the local structure that makes design and verification manageable. Layer-native models retain the domain-specific semantics, constraints, and reasoning methods needed within each layer, whereas one flat universal model would discard those abstractions and recreate a monolithic search and proof problem. The required composition must therefore preserve each layer’s native structure while exposing the cross-layer choices, dependencies, physical effects, and correctness assumptions that can alter feasibility, objective value, or validity. A credible end-to-end model must satisfy three linked criteria.

Semantic Fidelity: Every represented realization must satisfy semantic preservation with respect to the declared tensor-workload meaning: its intended operations, observable results, dependencies, state, communication, and allowed dynamic variation. Software transformations, mappings, runtime choices, and hardware realizations may change how the computation is carried out, but they must remain within the behavior the workload definition permits. Without this continuity of meaning, optimization may improve the wrong computation and later verification has no stable claim to establish.

End-to-End Sufficiency: Layer-specific models remain indispensable because each exposes the structure needed for its own decisions while hiding unrelated detail. They become insufficient when a choice, cost, physical constraint, or correctness assumption crosses a boundary. A locally valid transformation may create a requirement another layer cannot represent, a physical limit may invalidate a software mapping, or a lower implementation may violate an assumption on which an upper correctness claim depends. The end-to-end composition must therefore retain the cross-layer facts that can alter configuration feasibility, objective value, or correctness, including an implementation path from workload intent to a technology-specific physical implementation under declared constraints and analysis conditions. This sufficiency must allow alternative configurations and implementations to be constructed and compared, the consequences of a choice or changed assumption to be traced across the stack, and decisions requiring coordination to be distinguished from those that can remain local. It must also make visible when choices become fixed during design or compilation and which behavior legitimately remains adaptive at runtime. Physical costs and operating limits may be empirical or uncertain; that uncertainty can be represented explicitly rather than promoted to a false guarantee. No optimizer or agent can reason about a consequential fact that the modeling framework has erased.

Selective Compositionality: End-to-end sufficiency does not require one flat whole-stack abstraction. The composition must preserve the layer-native abstractions and reasoning structure of each layer, expose consequential information through explicit interfaces, and hide internal detail that cannot change another layer's decision or assurance claim. If it exports too little, consequential dependencies disappear and cross-layer reasoning becomes unsound or incomplete. If it exports everything, the model recreates the monolithic complexity that layering was introduced to control. This selective interface abstraction is what may allow compositional optimization and verification to remain modular and scalable. The model exposes this structure; it does not itself choose the best candidate or prove that a candidate is correct.

Concretely, the composed model must define the cross-layer design space: supplied workload and technology parameters, selectable design parameters or configuration variables, their value domains, and the legality and feasibility constraints that determine valid configurations. It must represent established parameter dependencies and cross-layer constraints while distinguishing known dependencies from candidate or unresolved cross-layer interactions, so any decomposition into subproblems is justified rather than assumed. It must also connect configuration choices to objective functions through performance and cost models and resource-use relations, exposing the evidence needed for bottleneck attribution without presuming the active bottleneck. Finally, it must state representation and correctness invariants together with assume–guarantee interface contracts and refinement obligations. The model represents this admissible structure; agentic exploration may later estimate interaction strengths and refine bottleneck attribution, while verification later discharges the stated obligations.

These representational choices make the cross-layer problem structured, not automatically tractable. For optimization, encoding legality and feasibility constraints, parameter dependencies, and candidate decompositions allows later search to treat the design space as structured rather than as an opaque, flat high-dimensional space and to decompose it only when those relations justify doing so; objective and resource relations also expose candidate limiting resources for later prioritization. Agents may estimate interaction strengths and refine bottleneck attribution, but they do not create legal choices or valid decompositions. For verification, semantic-preservation relations, correctness invariants, interface assumptions and guarantees, and refinement obligations define what each boundary must preserve. They provide the basis for partitioning checks by layer and composing discharged obligations across boundaries instead of requiring one monolithic whole-stack proof.

The bounded research question is therefore: what is the smallest composition of layer-native models that satisfies semantic fidelity and end-to-end sufficiency without abandoning selective compositionality? The goal is not maximum detail. It is enough cross-layer information to preserve consequential choices, physical constraints, and correctness assumptions while retaining the abstractions that keep each local problem manageable.

2.1 Existing Modeling Foundations

Which existing models already satisfy parts of the three criteria, and where does each abstraction stop? The relevant literature is not one lineage converging on a universal model. It is a set of complementary foundations, each made useful by choosing what to expose and what to hide. We organize seven foundation families—tensor semantics, compiler representations, architecture models, hardware–software co-design, runtime adaptation, physical and manufacturing models, and contracts and refinement—into four groups and evaluate them against the three requirements defined in the opening of Section 2. In this discussion, a normative language or interface specification is not a machine-checked proof, and an analytical or empirically validated cost model is not a correctness guarantee.

A. Meaning, Transformation, and Mapping

Models of computation first show how restrictions can expose useful invariants. Synchronous dataflow represents computation as actors with fixed token-production and consumption rates, allowing valid schedules to be constructed before execution while abstracting actor payloads [R10]. StableHLO addresses a different level: it specifies tensor operations, types, shapes, effects, execution, and forms of dynamism as a portable contract between ML frameworks and compilers [R34]. Synchronous dataflow exposes rates and dependencies but not tensor numerical meaning; StableHLO preserves much more workload meaning but does not prescribe a storage layout, schedule, resource mapping, or physical implementation.

Compiler representations make many of those implementation choices explicit. Halide established the separation between a functional algorithm and a performance schedule [R35]. MLIR, the Multi-Level Intermediate Representation, provides extensible dialects and intermediate representations that can coexist at multiple abstraction levels during progressive lowering [R36]. TVM exposes graph and operator transformations, schedules, target intrinsics, and memory scopes, while TensorIR represents multidimensional buffers, loop nests, computational blocks, access regions, dependencies, and tensorized hardware primitives [R37, R38]. Their systems evidence shows that explicit schedule and mapping choices can produce strong performance across heterogeneous targets. That evidence is principally compiler construction and measured performance, however: MLIR infrastructure does not by itself prove a dialect conversion correct, and performance validation of TVM or TensorIR does not establish semantic refinement through runtime, register-transfer-level (RTL) hardware, and physical realization.

These foundations therefore contribute semantic fidelity and selective compositionality at the workload and compiler levels. Their shared boundary is that the target architecture and its physical feasibility are largely supplied rather than derived, while the correctness and consequence of each cross-representation transition must be established separately.

B. Architecture, System, and Runtime Realization

Architecture-level models expose how a tensor mapping uses computation, storage, and communication. Timeloop represents regular operation spaces, hardware topologies, memory hierarchies, constraints, and mapspaces; MAESTRO uses data-centric directives to describe spatial and temporal mappings and infer reuse, traffic, execution time, and energy consequences [R39, R40]. These models support rapid comparison of large mapping and architecture spaces. Their results are analytical projections with validation and case-study evidence, not semantic proofs or physical signoff. They assume that the workload, mapping directives, hardware parameters, and component-cost data supplied to them are the right ones.

System-level foundations broaden the boundary. Metropolis separates functional behavior, architecture, mapping, schedulers, and quantitative annotations within one metamodel, while SystemC transaction-level modeling standardizes communication between behavioral components at deliberately reduced detail [R41, R42]. They demonstrate that layer-native models can be connected without flattening them. They do not determine automatically which hidden facts become consequential for a tensor objective, nor do their interface mechanisms prove that every user-supplied mapping preserves tensor meaning or reaches a valid physical instance.

Full-stack co-design systems establish a stronger constructive precedent. Gemmini links a parameterized tensor accelerator, a RISC-V system, a software stack, full-system simulation, and physical-design feedback; the public evidence includes full-system RTL simulation, physical-design results, and reported tapeouts and fabricated instances [R43]. This directly rules out the claim that meaningful end-to-end co-design paths are absent. Its boundary is instead scope: one accelerator-generator and software ecosystem supplies much of the structure internally. The evidence does not establish a general composition across independently evolving workload, compiler, runtime, architecture, package, process, and manufacturing models.

Runtime systems then model decisions that cannot be fixed earlier. Pollux co-adapts training configurations and cluster allocations using empirical throughput and statistical-efficiency models, while PagedAttention makes dynamic key-value (KV) cache block allocation explicit for language-model serving [R44, R26]. These systems demonstrate useful residual adaptation, but they begin from deployed hardware and compiled software. Their performance models do not state a general semantic envelope for allowed adaptation or carry physical-design and manufacturing assumptions back into runtime control.

C. Physical Implementation, Technology, and Manufacturing

Physical-design and semiconductor models expose consequences that architecture-only estimates cannot settle. OpenROAD's 2019 Alpha-flow design brought logic synthesis, floorplanning, placement, clock-tree synthesis, routing, timing, parasitic extraction, and power-integrity analysis into one public architecture aimed toward RTL-to-layout-data (GDSII) generation [R45]. A process design kit (PDK) supplies the technology-conditioned devices, interconnect assumptions, design rules, libraries, and extraction models that make such a flow meaningful. ASAP7 demonstrates this role for academic advanced-node research while explicitly remaining predictive, not tied to a foundry, and non-manufacturable [R46]. It is evidence that every physical result must retain its technology and model provenance, not evidence for a commercial 7-nm implementation.

Other physical and manufacturing models expose orthogonal constraints. 3D-ICE maps stack geometry, materials, cooling, and spatial power into transient temperature estimates and reports validation against measurements from a liquid-cooled 3D IC [R47]. Chiplet Actuary models die yield, die-to-die overhead, packaging, recurring and nonrecurring cost, reuse, and heterogeneous technology assignment for multi-chip systems [R48]. The first supplies physics-conditioned thermal evidence; the second supplies parameterized economic and yield analysis. Neither establishes functional correctness, electrical signoff, or the validity of an upstream tensor mapping.

These models are consequence-rich but semantically downstream. Even when used early for pathfinding, they usually receive RTL, layout, power maps, stack geometry, defect assumptions, and package choices after many workload and architecture decisions have been encoded elsewhere. Their central composition gap is therefore bidirectional: the path downward must explain how tensor and mapping choices produce these physical inputs, and the path upward must expose which physical limits or uncertainties invalidate or reshape earlier choices.

D. Contracts, Refinement, and Verified Transformations

Contract and refinement theories provide the clearest foundations for connecting abstractions without erasing them. Interface automata represent temporal input assumptions, output guarantees, compatibility, composition, and refinement [R30]. The Instruction-Level Abstraction gives accelerator operations a hierarchical, software-visible formal semantics and supports equivalence checking between abstraction levels; 3LA uses that interface to generate compiler matching and instruction-level simulators for application-level accelerator validation [R49, R21]. Timeline types encode cycle-level availability, initiation, and structural-use constraints so statically scheduled hardware modules can be composed safely [R22]. These works establish real interface mechanisms, but each chooses a bounded observation: generic interaction, software-visible accelerator behavior, or static pipeline timing.

Verified tensor compilation establishes complementary semantic edges. High-level scheduling rewrites can be proved semantics-preserving in a pure functional tensor language, and a later compiler proves lowering from that language to an imperative loop-and-array representation [R14, R15]. These are machine-checked guarantees for their stated languages and transformations. They do not extend automatically to every downstream compiler pass, runtime protocol, RTL implementation, numerical hardware behavior, or physical instance.

The synthesis is summarized below.

The surveyed public evidence thus establishes strong local models and several substantial cross-boundary bridges. It does not establish their joint capability: a selectively compositional representation that simultaneously preserves declared tensor behavior, retains every cross-layer fact that can change feasibility, objective quality, or correctness, reaches a technology-conditioned physical realization, and bounds the variation left to runtime. This is a claim about what the reviewed public evidence demonstrates, not a claim that proprietary industrial flows or other partial end-to-end systems do not exist.

2.2 A Compositional Cross-Layer World Model

To pursue this joint capability, we propose a compositional cross-layer world model: a structured federation of layer-native models connected by explicit cross-layer relations. Each member retains the representations and reasoning principles native to its layer, while the relations expose information whose consequences cross layer boundaries. In this paper, world model names that compositional representation. It is neither a learned simulator nor a universal intermediate representation, and it does not search candidates, discharge obligations, or validate physical claims.

The federation relates four typed configuration and assurance spaces. Compatible partial assignments that satisfy the structural constraints form configurations in the candidate space; a structurally legal or well-formed candidate is model-admitted for evaluation only under declared assumptions and validity ranges. The accepted/certified space contains only candidates whose required obligations have been discharged under declared rules, assumptions, and trusted bases. Within that space, certified status is reserved for a named certification criterion and its specified evidence; the model records these statuses but cannot confer them on itself. Deployment binds an accepted configuration to a target and workload context, producing a configuration in the deployed space; that configuration in turn induces the runtime space of permitted states and actions. Separately, every selectable design or configuration variable has a value domain and one of three commitment stages—design time, compilation/launch time, or runtime—while supplied workload and technology parameters remain inputs rather than choices. Physical validation or signoff supports only the physical claims established by named evidence and analysis conditions.

Within these spaces, the model represents structural dependence relations and hard cross-parameter constraints separately from assumed, predictive, measured, or unresolved interactions. These relations expose a candidate decomposition only when the constraints and objective relations support useful grouping and each known or candidate cross-group effect admitted by the representation is represented or conservatively bounded. Completeness of that relation set remains an adequacy question rather than a fact the model establishes by construction. Such a decomposition does not reduce the raw number of configurations; it may structure the effort required to explore them. Evaluators and profilers estimate or measure interaction strengths, and optimizers use those results to propose and search configurations. The world model represents this structure but does not determine the active decomposition.

The model also connects choices to objective functions through performance and cost models, resource-use relations, and technology-specific physical models. Each relation must retain its input and output meaning, assumptions, analysis conditions, evidence type, validity range, and uncertainty, and must distinguish declared quantities from predictions and observations. These relations expose candidate limiting resources and bottleneck indicators. They do not establish an active bottleneck or a physically valid implementation without the corresponding evaluation or physical evidence.

For compositional correctness, cross-layer relations declare semantic-preservation or observational-refinement relations, correctness invariants, interface assumptions and guarantees, compatibility conditions, and refinement and validation obligations. These declarations identify candidate verification boundaries. Partitioned verification additionally requires compatible assumptions and guarantees, an appropriate refinement relation, and a sound composition rule. A verifier discharges named obligations and establishes acceptance or a scoped composed claim only relative to the declared rules, assumptions, and trusted base; the world model neither performs that work nor turns empirical validation into formal proof.

The proposal is therefore conditional: the federation may expose a useful decomposition of search effort and candidate boundaries for partitioning verification obligations while preserving layer-native abstractions, but the distinct conditions for each must be established independently. It does not make the raw design space smaller, guarantee model accuracy or a global optimum, or establish manufacturability or signoff without named evidence. Its claim is that the required structure can be represented and tested rather than assumed.

2.3 Making the World Model Concrete: Research Questions

The proposed federation turns on four unresolved questions about the adequacy of its representation.

Admissible configurations and commitment. What typed relations can connect partial assignments in layer-native models to the candidate, accepted/certified, deployed, and runtime spaces without confusing assurance status with per-choice commitment? An answer must state how compatible partial assignments form a structurally legal or well-formed candidate, how declared assumptions and validity ranges govern model admission, how discharged obligations establish acceptance or—when a named certification criterion is met—certification, how deployment binds an accepted configuration, and how that binding induces a residual runtime envelope. In parallel, it must preserve whether each variable is committed at design time, compilation/launch time, or runtime. The runtime envelope must define the available observations, actions, state transitions, allowed semantic or numerical variation, and invariants without reopening rejected design alternatives.

Dependency structure and conditional decomposition. What conservative representational condition permits a candidate partition without discarding cross-partition constraints or unresolved interactions? An answer must distinguish structural or proved relations from assumptions, predictive or measured interactions with bounded validity, and unresolved dependencies that must remain conservatively coupled. It must state the objectives and conditions relative to which a grouping is proposed, the admitted cross-partition effects that must be represented or bounded, the adequacy obligation on the relation set, and when the grouping becomes inadmissible. Estimating interaction strength and using the resulting structure to guide search remain responsibilities of Section 3.

Consequence models and physical validity context. How can heterogeneous performance, cost, resource, and physical models align their input and output semantics across abstraction levels without treating unlike evidence as interchangeable? An answer must bind every declared, predicted, or observed quantity to its assumptions, analysis conditions, evidence type, validity range, and uncertainty, and must relate low-level observations to the semantic resource quantities used by cross-layer reasoning. It may expose bottleneck indicators and candidate limiting resources, but bottleneck prioritization belongs to Section 3, while physical feasibility, manufacturability, and signoff require the named evidence considered in Section 5.

Selectively compositional interfaces. What boundary information is sufficient relative to named workload observations, optimization objectives, and correctness properties, and what explicit criterion makes one sufficient interface selectively smaller than another? An answer must propose a relation under which compatible assumptions and guarantees, semantic-preservation or observational-refinement relations, and discharged obligations allow local claims to imply a scoped composed claim while irrelevant internal detail remains hidden. The model declares the proposed interfaces and relations; Section 4 owns the sound verification rules and methods that establish whether those claims compose.

Together, these questions define the representation: Section 3 addresses how agents estimate and exploit its search structure, Section 4 how its obligations and composition claims are verified, and Section 5 whether its adequacy, predictive validity, and tractability withstand evidence.

3. Agentic Optimization

Agentic optimization addresses the end-to-end design complexity of turning a tensor workload into a realizable system configuration. Given the workload, target technology, machine context, and environmental conditions, it must propose coherent configurations spanning hardware organization, system and software deployment, compiler mapping and kernel realization, and the bounded scheduling or resource-allocation choices left to runtime. The output is a candidate configuration that satisfies the world model's declared structural and feasibility constraints; physical feasibility, correctness, and acceptance still require the corresponding tool and verification evidence.

This design problem is difficult because the software–hardware cross-product is heterogeneous, its important interactions and bottlenecks are only partially known, and evaluating one choice may require compilation, distributed profiling, architecture simulation, high-level synthesis, or placement and routing. Treating all variables as flat and independent wastes evaluations and can miss consequences revealed only after lowering. The agent therefore needs the world model as a scaffold: declared variables and domains, constraints and environmental assumptions, known and unresolved dependencies, candidate decompositions, objective and resource relations, and evidence context. It may learn how to search this represented space or propose that the model is missing a consequential variable; it may not unilaterally create legality or change the evidence required for acceptance.

Cross-Layer Synthesis: This responsibility manages end-to-end design complexity by constructing one coherent hardware, system-software, compiler, and runtime-schedule configuration from the workload rather than optimizing independent layer choices that may be mutually inconsistent. Accelerator arrays, buffers, and interconnects must agree with placement, sharding, fusion, layout, tile shape, memory scope, generated kernels, and the permitted runtime action envelope. Every assignment remains conditional on declared workload assumptions, technology context, environmental conditions, variable domains, and hard constraints. Cross-layer synthesis preserves layer-native artifacts while making their consequential dependencies part of one candidate.

Self-Evolving World-Model Learning: This responsibility may reduce effective optimization complexity by using iterative compiler, profiler, simulator, high-level-synthesis, and physical-design feedback to discover or validate empirical decision boundaries, determine which represented or candidate variables are consequential, refine dependency and interaction hypotheses, identify conditionally separable subspaces, and attribute performance to limiting resources. Each learned relation retains its artifact, workload, target, tool, uncertainty, and validity context. Such learning can reprioritize proposals, refine an empirical decomposition, or trigger a separate world-model revision; it does not reduce the raw cardinality of the design space, and it cannot redefine workload semantics, hard constraints, verification obligations, or evidence authority.

Verification-Governed Synthesis: This responsibility controls correctness risk while agents explore a complex design space. Agents propose only configurations consistent with declared structural rules, resource bounds, workload assumptions, technology conditions, and environmental constraints, then submit the resulting compiler, kernel, hardware, and physical artifacts to the applicable checking and admission procedures. Compilers, tests, profilers, simulators, synthesis tools, and physical-design flows establish only their named, scoped results; verification tools discharge stated obligations, and the admission process establishes scoped acceptance. Rejection can guide the next proposal, but the agent cannot certify its own output or relax the condition that rejected it.

The causal mapping is therefore explicit. The world model represents the variables, constraints, dependency structure, objectives, evidence types, and verification obligations that make coherent synthesis possible; the optimizer uses that structure and accumulated feedback to concentrate effort on consequential choices; the verifier determines whether a proposed realization satisfies the required claim. This organization makes search structured and potentially improvable, not automatically tractable or globally optimal. It helps only when consequential relations can be represented, empirical interactions remain stable enough to learn, and tool feedback is informative at an affordable cost; dense hidden coupling or nontransferable evidence can eliminate the advantage over matched Bayesian, evolutionary, or solver-based search.

3.1 What Existing Systems Establish

Existing systems establish bounded mechanisms for the three responsibilities above, but not their composition from tensor workload through physical realization. In tensor compilation, the Tensor Language Model learns a proposal distribution over compiler-defined scheduling decisions and, under its reported workloads and protocol, matches fully tuned Ansor and MetaSchedule performance with substantially less compilation time [R50]. Meta LLM Compiler provides complementary adaptation evidence for LLVM intermediate representation and pass selection [R51]. These results show that domain-specific representations and training can improve proposals within an externally defined compiler space; they do not show that a language model should define the legal space. Ansor and MetaSchedule already combine domain-structured spaces with evolutionary or learned search, so they remain necessary non-agentic comparators for any claim that an agent reduces effective optimization complexity [R71, R72].

Tool-grounded kernel systems show how iterative evidence can reveal structure without transferring correctness authority to the agent. KernelBench couples proposed CUDA or Triton implementations to compilation, randomized correctness tests, execution timing, and optional profiling; its initial study found that frontier models produced kernels that were both correct under its tests and faster than the eager PyTorch reference on fewer than 20% of its 250 workloads, although iterative execution and profiling feedback improved some workflows [R54]. TritonGym makes compile, check, and profile access explicit so model and workflow effects can be compared under a common interface [R55]. Autocomp similarly combines accelerator-specific optimization menus with correctness and performance feedback across three workload categories on two tensor accelerators [R53]. Astra divides an existing SGLang-kernel loop among testing, profiling, planning, and coding roles [R58]. These systems support structured proposal, measurement, and revision over concrete kernel artifacts. They also expose the authority boundary: compilation, finite tests, profiling, and timing establish only their named results, not semantic equivalence. KernelBench-Verified demonstrates the practical consequence by adding hidden input distributions, a stronger Tensor Core baseline, and memory metrics; under that protocol, the best reported single-turn model falls from a 1.43x to a 0.88x geometric-mean speedup, and 28% of its kernels increase peak memory [R56].

Systems spanning wider layers provide bounded precedents for cross-layer synthesis. PROMPTS uses HLO operator profiles, roofline analysis, documentation, and past optimizations to propose sharding configurations for large-model training and serving [R59]. GPT4AIGChip connects generated accelerator choices to testbenches, high-level synthesis, synthesis estimates, and FPGA measurements, while LLM-DSE coordinates specialized roles over high-level-synthesis directives [R65, R66]. AutoChip uses compiler and simulation feedback to repair RTL, while ChatEDA and ORFS-agent invoke open EDA flows for tasks ranging from script generation to iterative floorplan, placement, clock, and routing parameter tuning [R64, R63, R67]. These systems show that agents can revise domain artifacts through compiler, synthesis, simulation, and physical-design loops. Tensor compiler, kernel, infrastructure, and accelerator results are direct evidence for bounded parts of the proposed stack; generic LLVM, RTL, and physical-design results provide adjacent mechanism evidence until transfer to tensor-system co-design is tested. A passing testbench, an HLS estimate, or an OpenROAD quality-of-result report remains scoped tool evidence, not functional verification, manufacturability, or signoff.

The same evidence sets a strict complexity claim boundary. Compiler-generated feedback can be less effective than repeated sampling at equal inference budgets [R52]. ArchGym finds that tuned random, Bayesian, evolutionary, and reinforcement-learning methods can become similarly competitive under different sample budgets and hyperparameters, while BOOM-Explorer provides a strong domain-informed, multi-objective Bayesian baseline for microarchitecture exploration [R69, R70]. HSCO-Bench reports that only two of five evaluated frontier models produced benchmark-valid end-to-end FPGA SoC prototypes under its build and test criteria, with substantial unused resources even among successful results [R68]. The surveyed multi-agent comparisons change model calls, context, tool access, or wall time together with role structure [R58, R59, R66]. Public evidence therefore supports bounded, tool-grounded proposal and revision; it does not yet establish that persistent learning or role decomposition reduces effective optimization complexity across the tensor stack. That claim requires matched comparison against domain-specific Bayesian, evolutionary, reinforcement-learning, solver-based, and repeated-sampling baselines.

The bounded evidence is summarized below.

3.2 A Model-Grounded, Provenance-Bearing Knowledge Base

Tool feedback can reduce effective optimization complexity only if the optimizer can determine which decision, artifact, target, and validity context each result describes. A knowledge base grounded in the Section 2 world model supplies that connection instead of treating prior runs as undifferentiated prompt history. For a kernel result, it retains the tensor operation and shapes, code revision, compiler flags, GPU and software versions, correctness procedure, timing samples, profiler counters, and numerical tolerance. For an accelerator result, it additionally retains the mapping, array and buffer parameters, high-level-synthesis or simulation version, resource report, and target device. For a physical result, it retains the RTL, netlist, layout, constraints, libraries, rule decks, process design kit, modes and corners, extracted parasitics, floorplan or placement checkpoint, EDA-tool version, raw reports, and the conditions and named checks under which timing, power, area, thermal, congestion, design-rule, or layout-versus-schematic results were produced. This scope lets an agent ask whether two observations support the same dependency or bottleneck hypothesis before reusing either one.

The knowledge base must keep five content classes distinct because search guidance and acceptance carry different authority. A declared contract comes from the world model: workload semantics, variable domains, hard constraints, objectives, and verification obligations. An unevaluated proposal records a candidate change, plan, or hypothesis before tool evidence exists. A raw observation comes from a named compiler, test, profiler, simulator, synthesis tool, physical-design flow, checker, or measurement and retains provenance and validity context. A derived empirical hypothesis relates observations within a stated scope and uncertainty—for example, that a tile-size and memory-scope interaction is active for one shape family, that register pressure limits a kernel, or that clock target and utilization should remain coupled during placement. Finally, a discharged-obligation or certification record may be written only by the verification and admission process of Section 4. Agents may use the first four classes to rank proposals or request a discriminating run, but they may not overwrite observations, change evidence class, or issue the fifth class.

Provenance must drive invalidation, not only auditing. The artifacts form a dependency graph: changing a tensor layout, buffer, RTL block, constraint, tool version, library, or process corner forks the candidate lineage and marks dependent binaries, simulation results, synthesis reports, and place-and-route evidence stale for the new branch. The immutable observations remain available for comparison, but they cannot support the revised candidate unless an explicit compatibility relation preserves their validity. The same rule applies to a learned interaction or bottleneck hypothesis derived from those observations. This prevents apparent search improvement from depending on evidence whose workload, toolchain, architecture, or physical assumptions no longer hold.

Existing systems supply partial precedents. AlphaEvolve retains candidate programs, evaluation results, and lineage in an evolutionary database [R60]. ORFS-agent retains checkpoint-aligned physical-design trajectories [R67], and PROMPTS retrieves documentation and historical optimizations [R59]. FlashInfer-Bench goes further for inference kernels by separating versioned definitions, workloads, solutions, and immutable evaluations, with compatibility metadata and kernel fallback or rollback [R61]. The surveyed evidence does not establish a provenance-typed knowledge base spanning tensor semantics, compiler and runtime decisions, accelerator artifacts, and physical evidence. The open question is whether such a base can preserve enough context to make interaction and bottleneck hypotheses reusable without falsely generalizing across shapes, GPUs, compiler versions, accelerator instances, process technologies, or physical corners.

3.3 Bounded Self-Evolution and Domain-Specific Model Adaptation

Self-evolution is the bounded mechanism by which repeated compiler, profiler, simulator, synthesis, and physical-design loops may reduce effective optimization complexity across later tasks. It improves proposal, planning, retrieval, or evaluation-selection policies from accumulated tool-grounded experience; possible updates include search heuristics, empirical interaction estimates, bottleneck hypotheses, retrieval indices, and proposal-model parameters. These changes may concentrate evaluations on performance-relevant subspaces, but they do not change the represented design space or the authority boundary. Tensor semantics, variable domains, hard constraints, verification obligations, certification rules, trusted checkers, and evidence status remain externally governed. A candidate that violates declared workload semantics while exploiting an incomplete kernel test distribution has exposed an evaluation defect, not learned a better design rule. Optimization for a declared deployment distribution is legitimate only within that stated semantic and assurance scope.

Four adaptation routes address different domain failures and must therefore be evaluated separately. Continued pretraining asks whether exposure to compiler intermediate representations and assembly, CUDA or Triton, hardware-description languages, EDA scripts, and architecture manuals improves structural fluency; Meta LLM Compiler and ChipNeMo provide bounded adjacent evidence in compiler and chip-design workflows [R51, R62]. Supervised fine-tuning asks whether curated or tool-evaluated examples improve legal transformation, artifact repair, and well-formed tool calls. Retrieval and tool grounding supply volatile compiler documentation, target descriptions, design artifacts, and measurements without changing weights. Post-training from evaluated trajectories asks whether compilation, testing, profiling, simulation, synthesis, or physical-design outcomes improve long-horizon proposal and tool selection. CUDA-L1 provides direct kernel evidence for post-training and documents reward exploits, but its training and evaluation draw from the same KernelBench task collection, leaving task-family generalization unresolved [R57]. No cited result establishes one adapted model across compiler and kernel optimization, AI-infrastructure configuration, accelerator design, and physical implementation.

Adapted weights are not a substitute for the knowledge base: weights alone provide neither inspectable record-level provenance nor selective invalidation when a compiler, workload, target, library, or process context becomes stale. A domain-adapted proposal model therefore consumes a versioned knowledge-base snapshot and writes plans and hypotheses back as unevaluated proposals. Only named tool results create observation records, and derived empirical hypotheses retain their lineage. Each adapter or checkpoint needs a parent identity, training-corpus and trajectory versions, tool and reward versions, exclusion filters, adaptation settings, and evaluation receipt. It may enter proposal service only after regression tests on previously supported compiler, kernel, hardware, and EDA tasks; a failed gate rolls back the proposal policy or retrieval state without erasing the underlying observations.

The decisive comparison separates weight adaptation from retrieval delivery. Its four arms are a fixed general model with common tools, the same model with retrieval and common tools, a model adapted from the same base with common tools, and that adapted model with retrieval and common tools. Paired contrasts hold the task and world-model snapshot, source corpus or knowledge-base version, tool APIs, evaluators, and budgets fixed; adaptation data and training cost are the intervention and are reported separately. Held-out tasks must cross more than prompt instances: unseen operator families and shapes, compiler revisions, GPUs or accelerators, RTL blocks, and physical-design contexts test whether learned structure transfers. Outcomes include well-formed tool-call rate, structural model-admission rate, artifact compilation or materialization rate, named-test pass rate, tool-reported resource or physical-constraint violations, objective quality, sample and wall-time cost, regressions, catastrophic forgetting, and rollback frequency. Measured post-training improvement remains evidence about that model, trajectory distribution, toolchain, and task boundary; it is not verified design knowledge.

3.4 Multi-Agent Coordination and the Game-Theory Boundary

Multiple agents are useful only if domain specialization makes cross-layer synthesis more coherent or less costly than a centralized optimizer. A compiler role can propose fusion, layout, and schedule moves and interpret compiler- or checker-reported well-formedness; a kernel role can inspect generated code and profiler counters; an infrastructure role can relate sharding, placement, batching, and routing to step time or service-level objectives; an architecture role can examine compute, memory, and interconnect organization; and a physical-design role can interpret timing, congestion, power, and thermal reports. These roles coordinate through the same typed candidate, evidence, and hypothesis records, not through untraceable natural-language consensus. A coordinator may allocate tool budget, request a cross-layer intervention, or maintain Pareto archives over latency, throughput, energy, area, cost, and thermal headroom under one shared objective vector and declared selection policy. Dominance is comparable only for compatible targets, contexts, evaluator fidelities, and uncertainty; a predicted or HLS-estimated point may prioritize a higher-fidelity run but cannot dominate a measured or signoff-scoped point as though their evidence were interchangeable. Declared structural dependencies and proposal-time constraints remain model-admission conditions; resource, physical, or safety claims requiring tool or verification evidence remain external acceptance obligations rather than objectives a role may trade away.

The default formulation is therefore centralized, constrained multi-objective optimization. Specialized roles cooperate for one shared objective vector, and the system—not a vote among roles—routes candidates through declared constraints and required checks. Role decomposition may reduce effective coordination complexity when compiler, profiler, simulator, and EDA contexts can be compressed through typed artifact interfaces and when parallel tool latency exceeds synchronization overhead. It should fail when cross-layer coupling remains dense, artifacts become stale across handoffs, or roles duplicate expensive evaluations. Astra, PROMPTS, and LLM-DSE provide examples of cooperative role decomposition, but their evidence does not isolate role structure from extra context, calls, and tools [R58, R59, R66]. A causal test compares a single centralized agent with a multi-agent system under the same proposal model, knowledge, tools, evaluator budget, and wall time, and separately compares typed shared records with natural-language-only handoffs. Stale-reference errors, conflicting assignments, duplicate tool calls, handoff failures, coordination time, and evidence-compatible Pareto quality all count.

Game theory is not the default foundation for this coordination. It becomes relevant only when controllers have genuinely distinct objectives or service-level obligations, private or local information, independent action or allocation authority, and resource externalities that a central optimizer cannot simply resolve. Themis, for example, uses application-level bids and a central auction to allocate contended GPUs under a fairness objective [R73]. That is structurally different from giving one optimizer several cooperating compiler, kernel, and EDA roles. The research must first establish which authority pattern exists; the number of agents alone does not create a game.

3.5 Research Questions and Evidence Contract

Four mechanism questions test the three responsibilities in the Section 3 opening. Can cross-layer synthesis manage end-to-end design complexity better than layer-local or flat search? Given the same represented variables, move grammar, constraints, tools, and evaluation budget, a joint optimizer should produce internally consistent compiler, kernel, runtime, architecture, and physical assignments with fewer rejected handoffs and faster progress toward an evidence-compatible Pareto frontier. The comparison must separate this coordination effect from a larger candidate language: generating CUDA, RTL, or another artifact outside a baseline's grammar is a representation-expansion experiment, not evidence that one search method is better.

Can tool-grounded experience reveal reusable search structure? The optimizer must distinguish a stable cross-layer interaction or limiting resource from noise, tool error, and a context-specific effect, while preserving unresolved dependencies until controlled interventions justify a partition. Under identical stored content, provenance-conditioned retrieval with applicability filtering and dependency invalidation should be compared with untyped similarity retrieval. Deliberately close but incompatible records—different tensor shapes, compiler versions, GPU generations, accelerator instances, process kits, or corners—test whether learned structure improves held-out search and reduces rejected artifacts, misleading tool runs, and recovery cost rather than merely improving auditability.

Does model adaptation add value beyond retrieval and accumulate safely? Continued pretraining, supervised fine-tuning, and trajectory post-training must each be compared with the fixed-model and retrieval-only arms defined in Section 3.3. Sequential held-out tasks test whether the proposal policy reduces compiler-rejected artifacts, kernels failing named test distributions, tool-reported resource violations, and place-and-route timeouts or declared-constraint violations without detected exploitation under hidden, shifted, and adversarial checker probes. Gains must survive regression tests and remain recoverable by checkpoint and memory rollback.

When does role decomposition outperform centralized search? Specialized compiler, kernel, infrastructure, architecture, and physical-design roles must be compared with a single agent and tuned stochastic, evolutionary, Bayesian, reinforcement-learning, and solver-based methods. A game-theoretic comparison is warranted only when independently controlled actors, distinct utilities or obligations, private information or strategic reports, coupled-resource externalities, and allocation authority beyond a central controller occur together.

All four questions use verification-governed evaluation. The optimizer proposes candidates; named compilers, tests, profilers, simulators, synthesis and physical-design tools, and Section 4 verifiers establish only their scoped results. Search-method comparisons freeze the represented candidate space, move grammar, model-admission and acceptance rules, tools, information, and evaluator versions. Multi-fidelity budgets are explicit: failed and early-stopped candidates consume budget, and competing methods receive matched call allowances by tool class or matched cumulative evaluator cost, together with a common wall-time or compute ceiling. Reports separate compiler, test, profile, simulation, synthesis, and place-and-route calls and time; maximum parallelism; model tokens and compute; coordination overhead; and timeouts.

The primary outcomes keep authority transitions separate: rates of well-formed tool calls, structural model admission, artifact materialization, named-test pass, tool-reported resource or physical-constraint satisfaction, and verifier-established obligation discharge. Optimization outcomes are best-so-far quality and evidence-compatible Pareto hypervolume or frontier coverage versus both evaluations and wall time. Sequential outcomes include held-out transfer, false-transfer rate, regression, rollback, stale-reference errors, duplicate evaluations, and handoff failures. Failure to beat matched domain-specific search, failure to transfer beyond stored contexts, or gains that disappear under stronger correctness and resource checks would falsify the claimed advantage in the evaluated domain.

The first go/no-go experiment remains small: freeze one two-layer space for a fused tensor region, with compiler choices such as fusion, layout, and tile family connected to kernel choices such as block geometry and memory scope. Use compilation, static resource checks, and named semantic tests as lower-cost evaluators, and profiler-backed runtime measurement as the expensive evaluator. Across held-out shapes, compare a provenance-conditioned agent with matched Bayesian and evolutionary search over the same moves, then ablate applicability filtering. If the agent does not reduce false transfer or time to a fixed performance level under matched budgets, whole-stack integration is not yet justified. This experiment has not been run; the present Section 3 evidence is the bounded prior work surveyed above.

4. Layered Verification

Layered verification addresses a different complexity problem from design-space exploration: how to determine whether one candidate tensor-system realization may enter the accepted/certified space without proving every candidate or rechecking at runtime facts already fixed earlier. Acceptance requires scoped evidence that the realization preserves its declared computation and remains within its resource, implementation, and runtime conditions. Given a world-model contract and a proposed realization, assurance must connect tensor semantics to compiler mappings, hardware behavior, physical implementation, and the bounded actions still allowed after deployment. The intended result is not one universal proof. It is a chain of scoped claims whose assumptions, artifacts, evidence, and authority remain explicit.

The difficulty is that the relevant facts become available at different times and are established by different kinds of evidence. Tensor semantics and transformation relations are visible in software representations; concrete shapes, layouts, schedules, buffers, routes, and target identities become known during compilation or launch; RTL, netlists, layouts, process collateral, and silicon measurements belong to hardware realization; queues, arrivals, allocations, failures, and contention may remain dynamic. A monolithic proof would combine incompatible abstractions and state spaces. Independent local checks are not enough either: a lower artifact can pass its own checker while violating an upper assumption that was never exported. The assurance architecture must therefore place each obligation at the earliest horizon with sufficient information, then preserve the resulting assumption–guarantee and refinement links.

Design and Fabrication Assurance: This horizon controls reusable hardware and physical-implementation risk. Before fabrication, it must establish the required behavioral or transaction-to-RTL refinement, protocol and concurrency properties, reset and clock-domain obligations, synthesis equivalence, and physical release conditions for exact artifact versions. Simulation, emulation, formal checking, static timing, design-rule checking, layout-versus-schematic comparison, and other physical analyses contribute different evidence and must not be merged into one generic “verified” status. Fabricated-device test and characterization may later instantiate or narrow the hardware contract for a particular silicon population and operating range; they do not retroactively turn finite measurements into a universal proof.

Compilation and Launch Assurance: This horizon binds a tensor workload and a concrete mapping to a qualified target. It must establish the named semantic-preservation or refinement claims across the selected rewrites and lowering edges, then check the resulting shapes, layouts, dependencies, schedules, buffers, communication, synchronization, resource predicates, artifact identities, and permitted runtime envelope. A verified compiler may establish a theorem for its admitted language; translation validation may instead check one source–target pair; ordinary compiler acceptance establishes only the compiler's own structural rules. An unsupported case, timeout, or failed obligation is rejected or left explicitly inconclusive rather than inferred correct.

Runtime-Bounded Assurance: This horizon controls only the freedom that legitimately remains after deployment, such as admitted shape parameters, placement, routing, admission, batching, queue and memory allocation, and responses to declared faults or contention. An agent or learned controller may propose an action, but a version-bound guard must decide whether the action and next state remain inside the deployed envelope before any irreversible effect, within the action's worst-case decision budget. Rejection invokes a previously checked fallback or refusal path with bounded progress. A monitor that merely observes a finite prefix cannot establish an eventual property, and a performance predictor cannot waive a deterministic semantic, resource, or safety condition.

This partition may reduce effective verification complexity when tensor operations and observations are declared; geometry, dependencies, rates, addresses, and resource effects are fixed, parameterized, or conservatively bounded before execution; payload values do not alter the control or resource behavior being abstracted; and the remaining runtime state and actions form a compact envelope. Then hardware obligations can be reused across workloads, compilation can specialize them to one mapping, and runtime can check only changing facts. The raw complexity of an individual proof or checker is not automatically reduced, and the factorization fails when payload-dependent routing, shape, allocation, synchronization, or termination reintroduces hidden state; when geometry, queues, retries, or faults are unbounded; when physical assumptions are stale; or when local contracts lack a sound composition rule.

4.1 What Existing Verification Foundations Establish

Restricted models of computation establish the first causal premise. Fixed token-production and consumption rates make balance and static scheduling questions analyzable in synchronous dataflow, while general process networks do not inherit bounded scheduling or termination merely from being dataflow [R10, R12]. Affine iteration and access structure similarly enables machine-checked polyhedral code generation for a defined compiler edge [R13]. These results do not prove actor payload semantics, arbitrary parallel execution, or target resource sufficiency. They show instead that exact restrictions can replace some execution-history reasoning with symbolic relations known before runtime.

Tensor-specific verification carries that premise into optimization and mapping. Verified scheduling rewrites and verified lowering for a functional tensor language show that performance choices can remain flexible while their semantic effect is constrained by proved transformations [R14, R15]. Hyperblock scheduling for verified high-level synthesis uses an untrusted scheduler with a verified validator, separating proposal quality from correctness authority [R16]. Translation validation for affine Halide programs checks required writes, defined reads, and value equality for one generated implementation, while an SMT-based validator covers selected machine-learning compiler transformations rather than the entire MLIR pipeline [R74, R75]. TrainVerify uses stage-wise checking and shape reduction to verify distributed training plans at reported frontier-model scale, but its claim stops before generated kernels, collective libraries, floating-point execution, runtime faults, and hardware [R25]. These systems provide direct evidence that tensor regularity can reduce particular proof objects; none establishes a complete framework-to-silicon chain.

Different obligations require different checkers. GPUVerify proves modeled race and barrier-divergence properties for supported CUDA and OpenCL kernels, not tensor functional equivalence or numerical accuracy [R76]. Honeycomb statically validates a parameterized family of GPU-binary memory accesses and performs low-cost per-launch argument checks, but its guarantee is memory-region confinement under its AMD ISA and trusted-monitor assumptions [R77]. The Instruction-Level Abstraction supports equivalence checking between software-visible accelerator specifications and finite-state-machine implementations, while Timeline Types check cycle-level composition for statically scheduled hardware [R49, R22]. Kami demonstrates machine-checked modular refinement for parameterized hardware families, and ABC provides combinational and sequential circuit-equivalence and model-checking machinery [R82, R83]. Together these works establish useful semantic, concurrency, timing, and hardware-refinement edges. Their properties compose only if their observation relations, assumptions, artifacts, and trusted bases are compatible.

Simulation and physical realization provide indispensable but different evidence. Application-level validation through a formal accelerator interface can expose whole-application defects, yet a simulator agrees with RTL only after a separate relation to that exact RTL has been established [R21]. The Universal Verification Methodology standardizes reusable simulation environments, while clock/reset-domain and AXI standards define verification intent and protocol obligations; none proves conformance merely by being adopted [R84, R85, R86]. OpenROAD and OpenLANE demonstrate reproducible paths through synthesis, placement, routing, extraction, timing, and layout checks, but an open flow or predictive process design kit is not commercial foundry signoff [R45, R46, R87]. Post-silicon quick-error-detection methods and deployed TPU measurements show the value of fabricated-device evidence, while remaining bounded to named instruments, devices, workloads, and conditions [R88, R9]. Functional proof, physical release, and measured-silicon qualification therefore remain separate claims.

Runtime systems expose both the opportunity and its boundary. StableHLO distinguishes bounded, unbounded, input-derived, and data-dependent dynamism; size-dependent array types discharge a useful subset of shape relations before execution [R19, R18]. JANUS guards speculative graph specialization and defers state updates so a failed assumption can fall back to imperative execution [R78]. TensorRT binds serialized engines to runtime versions and device capabilities, illustrating artifact compatibility checks without establishing semantic equivalence [R81]. PagedAttention manages dynamic key-value-cache allocation, and Clockwork uses profiled action windows to reject work predicted to miss a service deadline [R26, R79]. These are concrete late-bound mechanisms, not formal runtime guarantees. MegaBlocks is the counterexample: token values can determine expert routes and work even when surrounding tensor ranks are known [R27]. Finite-prefix runtime verification may also remain inconclusive, while supervisory control and shielding can enforce only properties represented by a sound observable model and an interceptable action set [R80, R29, R24].

The distinctions among these foundations are summarized below.

The surveyed foundations thus establish strong local proofs, validators, guards, physical analyses, and fallback patterns. The missing capability in the surveyed public evidence is their disciplined composition: one versioned assurance chain that places each obligation at the right horizon, binds every claim to its artifact and validity domain, permits only a compact residual runtime freedom, and invalidates downstream claims when an upstream assumption changes. This is not a claim that industrial flows lack end-to-end verification practice. It is the narrower observation that the joint tensor-specific composition and its complexity benefit have not been established by the evidence reviewed here.

4.2 A Three-Horizon Compositional Assurance Architecture

We propose a versioned assurance graph over the world model's candidate, accepted/certified, deployed, and runtime spaces. Its nodes are concrete semantic, compiler, runtime, hardware, physical, and silicon artifacts; its edges state the observation or refinement relation, upper assumptions, lower guarantees, compatibility conditions, and evidence required to discharge one obligation. The graph identifies what must be checked and where claims may compose. It does not certify itself: proof kernels and validators discharge formal obligations, admission procedures establish scoped acceptance, release authorities decide fabrication, and named physical or silicon evidence supports physical claims.

Evidence status must remain property-specific. A mechanized theorem establishes only its stated proposition under its formal semantics and trusted proof stack. A translation validator establishes a relation for one bound source–target pair. A compiler acceptance result establishes only syntax, typing, operation, shape, attribute, or target rules implemented by that compiler. A test or simulation samples concrete or modeled executions; a profiler or measurement records named executions and conditions. Synthesis, timing, power, thermal, and physical-design tools produce model-, target-, constraint-, mode-, and corner-conditioned evidence. Design-rule, layout-versus-schematic, timing, electrical, test, and silicon-characterization results each support only their named claims. An agent may use any of these records to propose the next action, but it may not upgrade their evidence class.

At the design and fabrication horizon, the hardware contract presented for acceptance should cover the software-visible operation semantics, transaction and ordering behavior, numerical mode, reset and fault behavior, finite resources, timing interface, and environmental assumptions that later mappings rely on. Selected relations then connect behavioral models to RTL, RTL to synthesized and engineering-change-order netlists, and those artifacts to the physical release packet. Formal refinement, protocol and concurrency checks, simulation regressions, clock/reset analysis, logic equivalence, static timing, geometry/connectivity checks, power-integrity and thermal analyses, and test collateral remain separate obligations. Any unresolved correctness-critical counterexample or failed required obligation blocks fabrication; an inconclusive result requires an accepted alternative evidence path or explicit narrowing of the feature or contract. After fabrication, test, repair, binning, calibration, and characterization bind actual device identities and operating ranges to a qualified subset of the contract. A contradiction triggers disablement, derating, remapping, or rebinding—not relabeling the observation as proof.

At the compilation and launch horizon, one workload and mapping are bound to that qualified hardware contract. The compiler may use previously proved transformations, or an untrusted optimizer may emit witnesses or certificates checked independently. The resulting assurance record names the source semantics and numerical observation, rewrite and lowering evidence, shape family, layout and storage remapping, dependence and lifetime conditions, distributed partition and collective model, kernel concurrency properties, buffer and communication bounds, target resources, runtime and checker versions, hardware identity, and residual runtime envelope. Proof-carrying code provides the general producer–checker pattern [R23]; tensor translation validators, TrainVerify, GPUVerify, and Honeycomb show why several property-specific checks are still needed. The technical output is a bound evidence record. The applicable admission or certification authority records scoped acceptance/certification, rejection, or an inconclusive status; only the first may authorize deployment. A plan that merely compiles, deserializes, passes sampled tests, or fits an analytical resource model has not thereby discharged the other obligations.

At the runtime horizon, the deployed contract exposes only bounded observations, actions, state transitions, and faults. A choice may remain dynamic only when its version-bound guard can decide membership and preservation of the next-state invariant from observable state before irreversible effect, within a declared worst-case decision time, and when refusal invokes a checked fallback that preserves bounded progress. Shape-family membership, queue capacity, key-value-cache blocks, placement, routing, admission, batching, and resource allocation are plausible runtime facts when their state and consequences are bounded. Payload-dependent expert routing, speculative updates, retries, and variable sequence growth require explicit bounds, rollback or deferred effects, and a progress rule. General liveness cannot be delegated to a finite-prefix monitor; it must be proved earlier or reduced to a bounded deadline, decreasing rank, retry budget, or guaranteed fallback. Performance predictions may choose among already admitted actions, but prediction error must cause only bounded performance degradation, not semantic or resource failure. The guard, its observation path, worst-case decision-time evidence, and fallback must themselves be accepted before deployment and rebound or invalidated when a relevant dependency changes.

Composition and invalidation are global even though checking is partitioned. A local claim contributes to acceptance only when its assumptions are established by preceding claims, its guarantees match the next interface, and a sound composition rule covers the desired observation. Every record binds hashes or versions of its specification, source and target artifacts, checker, solver or proof kernel, runtime, hardware, process collateral, constraints, modes, corners, and environmental assumptions as applicable. A changed layout, compiler, RTL block, netlist, process kit, corner, runtime, calibration, or fallback—or a violated validity premise such as an environmental excursion, device degradation, stale calibration, or breached fault assumption—must conservatively invalidate every possibly dependent claim unless a checked compatibility relation preserves it. Claiming an exact invalidation closure itself requires evidence that the represented dependencies are complete. The evidentiary trusted base therefore includes not “the tool” in general, but the contract semantics, proof kernels or result checkers, artifact-binding and invalidation mechanisms, unverified translators, reference models, environment assumptions, physical collateral, and runtime guard used by the named claim. Admission, certification, and release authorities are governance actors: they decide whether the scoped evidence is sufficient to proceed but cannot upgrade its evidence class.

The proposed architecture may factor assurance effort, but it does not guarantee that local obligations are small, that their assumptions compose, or that runtime checking is cheap enough. Its claim is conditional: static relations discharged earlier need not be re-proved at runtime, although mutable premises on which they depend may require monitoring. Uncertain performance behavior should remain outside deterministic correctness authority. Whether this partition produces a net complexity reduction is an empirical and formal question.

4.3 Making Layered Assurance Concrete: Research Questions

Four questions determine whether the three-horizon architecture is real rather than a relabeling of existing checks.

Where should each obligation be discharged? What criterion assigns semantic, numerical, dependence, lifetime, resource, protocol, refinement, physical, fault, and progress obligations to the earliest horizon with sufficient information while leaving only necessary freedom at runtime? A successful answer must derive the placement from commitment and observability, not from organizational ownership. It must identify the exact tensor restrictions—fixed or bounded geometry, controlled rates, affine or conservatively summarized accesses, payload-independent resource effects, and finite runtime actions—that allow an obligation to move earlier, and it must refuse the factorization when those restrictions fail.

When do local claims compose? What observation and refinement relations, assumption–guarantee compatibility rules, and trusted bases allow a tensor semantic claim, a mapping certificate, a hardware refinement result, a physical qualification record, and a runtime invariant to imply one scoped acceptance statement? The answer must keep mathematical or numerical equivalence, memory and concurrency safety, resource sufficiency, progress, and physical validity distinct. A sequence of passing tools is insufficient if an upper assumption is absent from the lower contract or if one check's model excludes a behavior relevant to the composed claim.

How do proof, checking, and invalidation costs scale? The central complexity test is not tensor size alone. It is whether certificate size, solver or checker time, trusted-state size, and rechecking closure scale with compact geometry and contract structure rather than payload volume, replica count, or full execution history. Matched variants should independently replace affine accesses with indexed accesses, fixed rates with payload-dependent work, bounded shapes with unbounded geometry, and payload-independent routing with value-dependent routing. Any timeout, unsupported case, or bounded no-counterexample result remains inconclusive unless the bound covers all admitted behavior. Cross-layer changes must also measure how much evidence is invalidated rather than assuming reuse.

Can runtime assurance remain both fast and useful? For one deployed envelope, the guard must be evaluated on worst-case and tail decision latency, state and observation overhead, rejected and corrected actions, fallback frequency and recovery cost, progress, and objective loss relative to an unconstrained oracle and a static safe policy. Hidden, shifted, stale, and adversarial conditions test whether the guard sees every consequential fact before action. If a monitor is often inconclusive, a fallback cannot meet the deadline, or checking overhead removes the benefit of adaptation, the claimed runtime freedom is not useful.

The first go/no-go experiment should bind one parameterized affine tensor region to one open accelerator or high-level-synthesis target and construct the smallest scoped prototype assurance chain: a workload semantic relation, one validated compiler mapping, explicit resource and concurrency checks, one behavioral-to-RTL obligation, versioned physical-flow evidence, and a launch/runtime guard over a bounded shape and allocation envelope. Across repeated launches and controlled artifact changes, compare it with a matched baseline that validates each concrete instance without reusing the partitioned claims. Measure total and amortized certificate-generation, proof or validation, interface-checking, runtime-guard, invalidation, and recovery costs; also report trusted-base size, guard worst-case latency, fallback behavior, and the evidence invalidated by one compiler, layout, RTL, and target-condition change. Then introduce one payload-dependent routing or unbounded-state variant without changing unrelated machinery. If local claims cannot be composed, if total assurance cost does not improve over the matched baseline, if checking cost still scales with payload-scale histories, or if the runtime guard must repeat the upstream proof, the three-horizon hypothesis fails for that region. This experiment has not been run; the current evidence is the bounded set of foundations surveyed above.

References

[R9] Norman P. Jouppi et al., “In-Datacenter Performance Analysis of a Tensor Processing Unit,” 2017. Google Research

[R10] Edward A. Lee and David G. Messerschmitt, “Static Scheduling of Synchronous Data Flow Programs for Digital Signal Processing,” 1987. DOI

[R12] Thomas M. Parks, Bounded Scheduling of Process Networks, 1995. PDF

[R13] Nathanaël Courant and Xavier Leroy, “Verified Code Generation for the Polyhedral Model,” 2021. DOI

[R14] Amanda Liu et al., “Verified Tensor-Program Optimization via High-Level Scheduling Rewrites,” 2022. DOI

[R15] Amanda Liu, Gilbert Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley, “A Verified Compiler for a Functional Tensor Language,” 2024. DOI

[R16] Yann Herklotz and John Wickerson, “Hyperblock Scheduling for Verified High-Level Synthesis,” 2024. DOI

[R18] Troels Henriksen and Martin Elsman, “Towards Size-Dependent Types for Array Programming,” 2021. DOI

[R19] OpenXLA, “Dynamism in StableHLO.” Specification

[R20] Haichen Shen et al., “Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference,” 2021. MLSys

[R21] Bo-Yuan Huang et al., “Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface,” 2024. DOI

[R22] Rachit Nigam, Pedro Henrique Azevedo de Amorim, and Adrian Sampson, “Modular Hardware Design with Timeline Types,” 2023. DOI

[R23] George C. Necula, “Proof-Carrying Code,” 1997. DOI

[R24] Mohammed Alshiekh et al., “Safe Reinforcement Learning via Shielding,” 2018. DOI

[R25] Yunchi Lu et al., “TrainVerify: Equivalence-Based Verification for Distributed LLM Training,” 2025. DOI

[R26] Woosuk Kwon et al., “Efficient Memory Management for Large Language Model Serving with PagedAttention,” 2023. DOI

[R27] Trevor Gale, Deepak Narayanan, Cliff Young, and Matei Zaharia, “MegaBlocks: Efficient Sparse Training with Mixture-of-Experts,” 2023. MLSys

[R29] P. J. Ramadge and W. M. Wonham, “Supervisory Control of a Class of Discrete Event Processes,” 1987. DOI

[R30] Luca de Alfaro and Thomas A. Henzinger, “Interface Automata,” 2001. DOI

[R34] OpenXLA, “StableHLO Specification.” Specification

[R35] Jonathan Ragan-Kelley et al., “Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines,” 2013. DOI

[R36] Chris Lattner et al., “MLIR: Scaling Compiler Infrastructure for Domain Specific Computation,” 2021. DOI

[R37] Tianqi Chen et al., “TVM: An Automated End-to-End Optimizing Compiler for Deep Learning,” 2018. USENIX

[R38] Siyuan Feng et al., “TensorIR: An Abstraction for Automatic Tensorized Program Optimization,” 2023. DOI

[R39] Angshuman Parashar et al., “Timeloop: A Systematic Approach to DNN Accelerator Evaluation,” 2019. DOI

[R40] Hyoukjun Kwon et al., “Understanding Reuse, Performance, and Hardware Cost of DNN Dataflows: A Data-Centric Approach,” 2019. DOI

[R41] Felice Balarin et al., “Metropolis: An Integrated Electronic System Design Environment,” 2003. DOI

[R42] Open SystemC Initiative, “TLM-2.0 Language Reference Manual,” version 2.0.1, 2009. Language reference manual

[R43] Hasan Genc et al., “Gemmini: Enabling Systematic Deep-Learning Architecture Evaluation via Full-Stack Integration,” 2021. DOI

[R44] Aurick Qiao et al., “Pollux: Co-adaptive Cluster Scheduling for Goodput-Optimized Deep Learning,” 2021. USENIX

[R45] Tutu Ajayi et al., “Toward an Open-Source Digital Flow: First Learnings from the OpenROAD Project,” 2019. DOI

[R46] Lawrence T. Clark et al., “ASAP7: A 7-nm FinFET Predictive Process Design Kit,” 2016. DOI; official project

[R47] Arvind Sridhar et al., “3D-ICE: A Compact Thermal Model for Early-Stage Design of Liquid-Cooled ICs,” 2014. DOI

[R48] Yinxiao Feng and Kaisheng Ma, “Chiplet Actuary: A Quantitative Cost Model and Multi-Chiplet Architecture Exploration,” 2022. DOI

[R49] Bo-Yuan Huang et al., “Instruction-Level Abstraction: A Uniform Specification for System-on-Chip Verification,” 2019. DOI

[R50] Yi Zhai et al., “Enabling Tensor Language Model to Assist in Generating High-Performance Tensor Programs for Deep Learning,” 2024. USENIX

[R51] Chris Cummins et al., “Meta Large Language Model Compiler: Foundation Models of Compiler Optimization,” 2024. Paper

[R52] Dejan Grubisic, Chris Cummins, Volker Seeker, and Hugh Leather, “Compiler Generated Feedback for Large Language Models,” 2024. Paper

[R53] Charles Hong, Sahil Bhatia, Alvin Cheung, and Yakun Sophia Shao, “Autocomp: LLM-Driven Code Optimization for Tensor Accelerators,” 2025. Paper

[R54] Anne Ouyang et al., “KernelBench: Can LLMs Write Efficient GPU Kernels?” 2025. Paper

[R55] Yue Guan et al., “TritonGym: A Benchmark for Agentic LLM Workflows in Triton GPU Code Generation,” 2026. OpenReview

[R56] Yunxiang Zhang et al., “KernelBench-Verified: Do LLM-Generated Kernels Actually Beat PyTorch?” 2026. Paper

[R57] Xiaoya Li, Albert Wang, Guoyin Wang, Jiwei Li, and Chris Shum, “CUDA-L1: Improving CUDA Optimization via Contrastive Reinforcement Learning,” 2026. Paper

[R58] Anjiang Wei et al., “Astra: A Multi-Agent System for GPU Kernel Performance Optimization,” 2025. Paper

[R59] Yuran Ding, Ruobing Han, Xiaofan Zhang, and Xinwei Chen, “PROMPTS: Performance Optimization via Multi-Agent Planning for LLM Training and Serving,” 2026. Google Research

[R60] Alexander Novikov et al., “AlphaEvolve: A Coding Agent for Scientific and Algorithmic Discovery,” 2025. Paper

[R61] Shanli Xing et al., “FlashInfer-Bench: Building the Virtuous Cycle for AI-Driven LLM Systems,” 2026. Paper

[R62] Mingjie Liu et al., “ChipNeMo: Domain-Adapted LLMs for Chip Design,” 2024. Paper

[R63] Zhuolun He et al., “ChatEDA: A Large Language Model Powered Autonomous Agent for EDA,” 2024. Paper

[R64] Shailja Thakur et al., “AutoChip: Automating HDL Generation Using LLM Feedback,” 2024. Paper

[R65] Yonggan Fu et al., “GPT4AIGChip: Towards Next-Generation AI Accelerator Design Automation via Large Language Models,” 2023. Paper

[R66] Hanyu Wang et al., “LLM-DSE: Searching Accelerator Parameters with LLM Agents,” 2025. Paper

[R67] Amur Ghose, Andrew B. Kahng, Sayak Kundu, and Zhiang Wang, “ORFS-agent: Tool-Using Agents for Chip Design Optimization,” 2026. Paper

[R68] Pei-Huan Tsai, Kuan-Lin Chiu, William Baisi, Pin-Yu Chen, and Luca P. Carloni, “HSCO-Bench: An Agent-Driven End-to-End Hardware-Software Co-design Benchmark for Systems-on-Chip,” 2026. Paper

[R69] Srivatsan Krishnan et al., “ArchGym: An Open-Source Gymnasium for Machine Learning Assisted Architecture Design,” 2023. Paper

[R70] Chen Bai et al., “BOOM-Explorer: RISC-V BOOM Microarchitecture Design Space Exploration Framework,” 2021. Primary PDF

[R71] Lianmin Zheng et al., “Ansor: Generating High-Performance Tensor Programs for Deep Learning,” 2020. USENIX

[R72] Junru Shao et al., “Tensor Program Optimization with Probabilistic Programs,” 2022. Paper

[R73] Kshiteej Mahajan et al., “Themis: Fair and Efficient GPU Cluster Scheduling,” 2020. USENIX

[R74] Basile Clément and Albert Cohen, “End-to-End Translation Validation for the Halide Language,” 2022. DOI

[R75] Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, and Juneyoung Lee, “SMT-Based Translation Validation for Machine Learning Compiler,” 2022. DOI

[R76] Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, and Paul Thomson, “GPUVerify: A Verifier for GPU Kernels,” 2012. DOI

[R77] Haohui Mai et al., “Honeycomb: Secure and Efficient GPU Executions via Static Validation,” 2023. USENIX

[R78] Eunji Jeong et al., “JANUS: Fast and Flexible Deep Learning via Symbolic Graph Execution of Imperative Programs,” 2019. USENIX

[R79] Arpan Gujarati et al., “Serving DNNs like Clockwork: Performance Predictability from the Bottom Up,” 2020. USENIX

[R80] Andreas Bauer, Martin Leucker, and Christian Schallhart, “Runtime Verification for LTL and TLTL,” 2011. DOI

[R81] NVIDIA, “TensorRT Engine Compatibility.” Documentation

[R82] Joonwon Choi et al., “Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification,” 2017. DOI

[R83] Robert K. Brayton and Alan Mishchenko, “ABC: An Academic Industrial-Strength Verification Tool,” 2010. DOI

[R84] IEEE, “IEEE Standard for Universal Verification Methodology Language Reference Manual,” IEEE 1800.2-2020. Standard

[R85] Accellera Systems Initiative, “Standard for IP Abstraction for Clock and Reset Domain Crossing Integration 1.0,” 2026. Standard

[R86] Arm, “AMBA AXI and ACE Protocol Specification,” IHI 0022H, 2020. Specification

[R87] Mohamed Shalan and Tim Edwards, “Building OpenLANE: A 130nm OpenROAD-Based Tapeout-Proven Flow,” 2020. DOI

[R88] Keith Campbell et al., “Hybrid Quick Error Detection: Validation and Debug of SoCs Through High-Level Synthesis,” 2019. DOI