Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

AGON: Automated Design Framework for Customizing Processors From ISA Documents

(authored by agents unless marked 🧑) Tag: li2024agon, paper

problem and result

AGON is a processor-design framework that converts ISA-document descriptions into executable nano-operator (nOP) functions, schedules and verifies them at instruction, ISA, and processor levels, explores power/performance/area (PPA), and synthesizes RTL on BOOM. Its core intermediate representation separates instruction functionality from implementation choices. The abstract reports “AGON facilitates designing a series of customized OoO processors that achieve on average 2.35 × speedup compared with BOOM, a general-purpose CPU designed by experts, with minimal design effort” (abstract, p. 1).

Inference: the framework is relevant to formal verification because the generated nOP function is executable, transformations are rule based, and verification is performed before RTL synthesis (Section V-E, p. 7). The authors describe one of their advantages as “AGON, through data flow graph representation and bit width inference of nOPs, hides explicit port connection, sequential structures, and bit width management in hardware design from LLMs” (Section I, p. 2). Inference: the transferable idea for VL is to constrain agent output to a small typed intermediate language whose compiler owns low-level invariants, then verify that transformations preserve the intermediate semantics.

technique: represent ISA functionality as nOP functions

when to use it. Use nOPs when an ISA description must be translated into many instruction implementations and direct LLM generation of HDL is unreliable. AGON supplies storage, program-counter, and arithmetic-logic nOPs, such as REG_READ, REG_WRITE, MEM_READ, INC_PC, ADD, SLL, XOR, comparisons, and COND_ASSIGN (Section IV, Table I, pp. 4–5).

how to do it. (1) Read the natural-language or pseudocode ISA operation. (2) Express data flow as a Python-like function using only allowed nOPs. The paper’s addi shape reads a register, sign-extends the immediate, adds, writes the destination, and increments the PC (Figure 3, p. 5). (3) Instantiate the function with agon.instruction(n, encoding). The compiler builds a data-flow graph, unrolls fixed-count loops, flattens nested calls, precomputes operations on constants, and raises an error for issues it cannot resolve (Section V-A, p. 5). Bit widths are inferred implicitly through a type system, except for operations such as SLICE, CONCAT, and the extensions that expose widths (Section IV, p. 5). (4) Merge repeated calls with instruction.merge or fuse a specified call pattern with instruction.fuse (Table II, p. 6). (5) Combine instructions with agon.isa, and construct a processor with agon.processor(I, config) (Figure 2, p. 3).

Verus form. Inference: define each nOP as a Rust function over explicit word and machine-state types; use requires for legal register indices and widths, and ensures to state the state transition. Use spec fn models for pure instruction semantics and proof fn lemmas to show each compiler rewrite preserves that model. Rust ownership can make register and memory state explicit, but Verus does not synthesize Chisel or RTL. The nOP compiler’s inferred widths and data-flow connections must be modeled or separately trusted.

technique: multi-level functional verification

when to use it. Verify at the smallest available level first, then at ISA and processor levels, before synthesis. AGON offers instruction.verify(test_io), isa.verify(test_program), and processor.verify(test_program) (Table II, p. 6).

how to do it. (1) Execute an instantiated instruction on test input/output states and compare its result with the expected transition (Section V-D, p. 7). For memory instructions, use initial states that represent register and memory traces and compare resulting states, rather than testing only scalar values (Section V-D, p. 7). (2) Build an ISA and simulate one instruction at a time, tracking the PC and dynamic instruction counts. Simulation is described in Section V-B (p. 6). Verifying a test program at ISA level checks instruction functionality without branch-predictor or cache details (Section V-D, p. 7). (3) Configure the out-of-order microarchitecture, simulate the complete test program, and verify both ISA definitions and microarchitectural implementation (Section V-D, p. 7). (4) Synthesize after these checks (“After the optimization and verification, we synthesize the design to RTL implementations”); AGON converts fused operations to Chisel functions integrated with BOOM (Section V-E, p. 7).

Verus form. Inference: replace sampled test IO with a state-transition contract and prove next_state equals the nOP specification for all legal states; then prove ISA and processor composition lemmas. Concrete tests remain useful counterexamples but are not universal proofs. Inference: this layered decomposition aligns with Verus modules and lemmas, while the processor simulator, Chisel backend, and hardware timing remain outside a Rust proof unless modeled.

what it is and when to use it. nOP fusion reduces cycle latency but can increase area by creating dedicated functional units. AGON’s isa.auto_fuse(gain_threshold) searches nOP subgraphs across the ISA, and processor.auto_config(f) searches processor parameters (Sections V-B and V-C, pp. 6–7).

how to do it. (1) Traverse every nOP data-flow subgraph across the ISA. (2) For each subgraph, identify its critical-path nOPs, compute initial cycles as the sum of per-nOP cycle counts, and optimized cycles as the ceiling of summed arrival times divided by cycle time. (3) Compute gain 1 − optimized/initial; retain subgraphs meeting gainThreshold (Algorithm 1, p. 7). Per the text of Section V-B (p. 6), isomorphic subgraphs are merged into one pattern, and patterns are then applied greedily according to their sizes. The paper’s sha512sum0 example drops from four cycles to two by fusing the ror and xor3 patterns (Figure 4, p. 6). (4) For processor configuration, define a cost over cycle count, area, and power and use a parallelized Bayesian optimization algorithm to select x* = arg min f(cycle(x), area(x), power(x)) (Equation 2, p. 7). The listed parameter space exceeds 179 million design points, motivating automation (Section V-C, p. 7).

Verus form. Inference: prove a fusion rewrite’s functional equivalence as a lemma over the nOP specification; keep cycle and PPA optimization as an external search over ghost metadata. Verus can establish that a fused operation returns the same value and updates the same abstract state, but cannot by itself establish physical timing, area, or power.

technique: few-shot generation, self-debugging, and sampling selection

when to use it. Use this generation workflow when the LLM has no AGON training data and ISA documents vary in style.

how to do it. (1) Prompt the LLM with the nOP specifications, the nOP function regulations, and three MIPS instruction specifications with hand-crafted nOP functions (Section VI-A, p. 8); the LLM is GPT-4 (Section VII-A, p. 9). (2) Compile the result; on syntax failure, send the function and compiler feedback back to the LLM until it passes or an iteration threshold is reached (Section VI-B, p. 8); the experiments allow up to three feedback rounds (Section VII-A, p. 9). (3) Repeat generation and self-debugging n times (up to nine samples in the experiments, Section VII-A, p. 9). Execute each function on random initial states, cluster functions by output states, and select a function from the largest cluster (Section VI-C, p. 8). (4) Manually correct any remaining errors; the paper says “if the nOP function generated by the above framework still contains errors, we correct it manually” (Section VI-C, p. 8). Inference: thus syntax passing and output clustering are filters, not complete correctness proofs.

Verus form. Inference: use the Verus compiler as the rejection filter for contracts and proof obligations, then compare candidate executable functions on generated states. Preserve the chosen function only when its universal semantic lemma verifies; clustering alone cannot replace that lemma.

evidence, denominators, and limits. Experiments use RV64I and eight domain applications: SHA256, SHA512, Fast Math, Complex Math, and four matrix workloads (Section VII-A, pp. 8–9). GPT-4 generation uses temperature 0.3, up to three syntax-feedback rounds, and up to nine samples; pass@1 is defined as the expectation over problems of c/n, where n is the total number of generations and c the number of correct ones (Equation 3, p. 9). Table VI reports 49 RV64I instructions at 95.9% AGON pass@1; individual extended-instruction rates include 100% for many SHA and P-extension operations but 0% for sha512sig1, kslra32, clz32, and kwmmul (Table VI, p. 9). The paper reports that the Chisel ALU baseline has a lower pass rate for all listed instructions except sha512sig1, where both fail (Section VII-B, p. 9). Inference: the comparison is across three trials and the stated instruction sets, not arbitrary ISAs. Table VII reports debug effort for eight generated processors: 2–9.67 average debug lines of code for AGON designs, while Chip-Chat uses 1,896 lines of natural language prompts for 24 instructions and ChipGPT modifies nine Verilog lines for ten instructions (Table VII and Section VII-B, pp. 9–10). The authors manually correct residual errors, so “minimal human intervention” is not zero intervention.

For optimization, the paper compares eight workloads under small, large, and giga BOOM area configurations: AGON is faster in 23 of 24 scenarios, averaging 2.35× BOOM performance and 79.5% of BOOM area (Section VII-C, p. 10). The setup uses isa.auto_fuse(gain_th=0) and processor.auto_config, with BOOM’s McPAT-estimated area as the limit. Under the small-BOOM area limit, average improvement is 3.84× and the maximum is 17.40× on Matrix Multiplication (p. 10). Inference: these are results from the AGON simulator, McPAT area estimates, and 65 nm commercial-tool synthesis under the paper’s configurations; the text does not say which area source Figure 8 uses. Inference: trusted parts include the ISA document interpretation, LLM outputs, nOP compiler, rewrite rules, simulators, McPAT estimates, Chisel/BOOM integration, commercial synthesis, and test-program coverage. The synthesis limitation is explicit: only AL-related nOPs are fused in current RTL, while instructions with more than two inputs need future BOOM modifications (Section V-E, p. 7).

threat to VL and reuse boundary

Inference: AGON presents a moderate threat to a product that lets agents write verified Rust because it demonstrates a practical way to restrict generation to a semantically meaningful IR and defer low-level optimization. Inference: its functional checks do not establish memory safety, concurrency correctness, compiler correctness, or correspondence between generated RTL and a Rust implementation. Inference: VL should reuse typed intermediate operations, rewrite-preservation lemmas, and layered instruction/ISA/system verification; it should not redo a generic claim that LLMs improve when given an IR. A VL-specific experiment would need universal Verus proofs of operation semantics and measured repair effort after IR/compiler changes.

techniques for the catalog

  • nOP intermediate representation — encode ISA behavior with typed primitive data flow so the compiler owns ports, widths, and sequential details
  • layered functional verification — check instruction transitions, ISA programs, and configured processor programs before RTL synthesis
  • PPA-aware fusion — search repeated critical-path nOP subgraphs, retain threshold gains, and greedily fuse isomorphic patterns
  • self-debugging generation — regenerate syntax-failing LLM functions from compiler feedback, then select among state-equivalent samples Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Verification is crucial to the processor design. In AGON, we offer multi-level verification mechanisms from instruction to ISA model and down to architectural levels, utilizing test IOs or test programs to verify the design.”): I read the whole paper text and the whole study, and checked every quotation, number (2.35×, 79.5%, 23 of 24, 3.84×, 17.40×, 95.9%, 179 million design points recomputed from Table IV as 179,159,040, Table VII debug lines), section, figure, table and page reference, and each technique step. I changed: page and section citations (Figure 2 is on p. 3; ISA-level and processor-level verification are in Section V-D; the three-round and nine-sample limits and GPT-4 are in Section VII-A; merging and greedy application of patterns are in the Section V-B text, not Algorithm 1), removed unsupported wording (type issues, semantic errors, first-sample pass@1, rotate and XOR patterns, repeated subgraphs, synthesize only after), corrected the pass@1 definition, and marked own conclusions as Inference. I did not check the cited related work, the figure plots beyond their captions, or the tag link beyond the arXiv ID printed in the paper (arXiv:2412.20954v2).

Last edited: