Overview

In the provided evidence, code generation refers to the automated or semi-automated production of executable code (or test programs) from higher-level inputs. The term spans at least three distinct research contexts that all appear in the supplied evidence:

• Compiler code generation — the back-end phase that translates a compiler's intermediate representation (IR) into target-architecture instructions using a set of rewrite rules. New evidence (the 2022 SMT-synthesis paper) shows that these rewrite rules can be automatically synthesized from an architecture's RTL using satisfiability-modulo-theories (SMT) solvers.
• LLM-based code generation — generating code (and, in the verifiable variant, also formal specifications and proofs of code-specification alignment) from natural-language problem descriptions using large language models. New evidence includes the GAP-Gen guided Python code generation system and the VERINA verifiable code generation benchmark.
• Functional-verification code generation — the use of automated or semi-automated tools that produce diagnostic instruction sequences (test programs) for the simulation-based functional verification of high-performance microprocessors. (This is the content preserved from the previous version of this article, drawn from the 1996 DAC paper.)

Compiler code generation

Back-end structure and the role of rewrite rules

Most compilers share a common structure: a front end translates a high-level language into an IR, an optimizer transforms the IR, and a code generator translates the IR into a hardware-specific representation (which may then be further optimized for the target architecture). The code generation stage typically involves instruction selection, scheduling, resource assignment, and assembly.

There has been significant work devoted to developing instruction-selection algorithms that use a set of pre-defined rewrite rules to translate IR programs to architectural instructions. These rewrite rules are dependent on the target ISA and are usually constructed manually. Every new ISA must therefore be accompanied by a set of rewrite rules that describe how to transform a compiler's IR to that ISA. Crafting these rules is a labor-intensive task that is often performed by hand and is difficult to keep in sync with a rapidly changing design.

A rewrite rule indicates the options for how to transform one or more IR instructions into one or more architecture-specific instructions. For example, an architecture supporting only a subtract instruction could be specified with an Arch predicate such as

(ite(inst = 00, y1 −[8] y2,
    ite(inst = 01, y1 +[8] y2, ...))

— an if-then-else encoding of an 8-bit ALU with two inputs and one output selected by an opcode inst.

SMT-based synthesis of rewrite rules from RTL

The 2022 paper Synthesizing Instruction Selection Rewrite Rules from RTL using SMT (Deshpande, Doko, Martínez, and Barrett) attacks the manual rule-writing bottleneck by deriving rewrite rules directly from an architecture's RTL. The key idea is to construct first-order logic queries whose solutions, obtained using an SMT solver, represent instruction-selection rewrite rules.

Why use RTL directly rather than a manual ISA specification?

• It avoids the manual specification step, which is particularly important for design space exploration, where maintaining both the RTL and a corresponding formal specification is difficult for a rapidly changing design.
• ISA specifications typically do not capture the instruction format or the instruction decode logic, both of which are needed for an end-to-end correctness argument.
• Using RTL presents unique challenges, which the paper addresses.

Contributions of the paper:

• Formalization of the correctness criteria for a general class of rewrite rules between arbitrary IRs and RTL-based architectures.
• A technique for supporting parametric rewrite rules.
• A method for abstracting complex operations whose semantics are either unknown or too costly to model directly (e.g., floating-point operations), which previous SMT-based approaches found prohibitively expensive.
• A methodology for efficiently encoding and solving the rewrite rule synthesis problem using SMT.

Reported case studies:

• Synthesizing rewrite rules from CoreIR (an IR designed for RTL) to a family of CGRAs.
• Synthesizing rewrite rules from WebAssembly to various RISC-V architectures, targeting both the base ISA and a number of extensions, including extensions with floating-point operations.
• All of these tasks could be done in seconds.
• The tool is also able to synthesize short multi-instruction sequences for pseudo-operations — RISC-V, for example, lacks equals/not-equals instructions and documents pseudo-operations such as (x - y) < 1 for unsigned less-than; it also lacks documented sequences for less-than-or-equals and greater-than-or-equals (which can be implemented as (y < x) ^ 1 and (x < y) ^ 1 respectively). Synthesizing these took at most 90 seconds.

The approach builds on the standard SMT machinery (Table I of the paper lists theory-specific notation for bitvectors, floating-point arithmetic, arrays, and algebraic data types — sorts such as BV[n], +[n], x[msb:lsb], ite(c,x,y), and so on).

LLM-based code generation

GAP-Gen: Guided Automatic Python Code Generation

GAP-Gen (2022, arXiv:2201.08810) addresses automatic code generation from natural-language descriptions. It is a guided method based on Python syntactic constraints and semantic constraints, and introduces two new structures:

• Syntax-Flow — a simplified version of the Abstract Syntax Tree (AST) that reduces the size and high complexity of an AST while maintaining the crucial syntactic information of Python code.
• Variable-Flow — abstracts variable and function names consistently throughout the code.

Rather than pretraining from scratch, GAP-Gen focuses on modifying the finetuning process, which reduces computational requirements while retaining high generation performance. It fine-tunes the transformer-based language models T5 and CodeT5 on the Code-to-Docstring datasets CodeSearchNet, CodeSearchNet AdvTest, and the Code-Docstring Corpus from EdinburghNLP. The reported experiments show that GAP-Gen achieves better results on automatic Python code generation than previous works.

VERINA: Benchmarking Verifiable Code Generation

VERINA (2025, arXiv:2505.23135) introduces the term verifiable code generation — jointly generating code, specifications, and proofs of code-specification alignment — as a promising path to address the fact that LLM-generated code often requires costly manual review to ensure correctness. The benchmark consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites, enabling a comprehensive and modular evaluation of code, specification, and proof generation, as well as their compositions.

Evaluation of state-of-the-art LLMs on VERINA revealed significant challenges, especially in proof generation. The best model evaluated, OpenAI o3, achieved:

• 72.6% code correctness rate
• 52.3% specification soundness and completeness
• 4.9% proof success rate (based on one trial per task)

The authors release the dataset at huggingface.co/datasets/sunblaze-ucb/verina and the evaluation code at github.com/sunblaze-ucb/verina, framing VERINA as a catalyst for progress on LLM-based theorem provers in verification domains.

Functional verification code generation (1996 DAC methodology)

This section preserves the content from the previous version of the article.

Functional verification context

Functional verification aims to isolate design and implementation flaws so that the design released to manufacturing is fully operational — the RTL model must exhibit the same behavior as an architectural simulator when executing the same instruction sequence. As the complexity of high-performance microprocessors grows (advanced execution mechanisms, complex external interfaces with multiple outstanding loads and stores, multi-level caches, and cache coherency in multiprocessor configurations), the DVT team becomes increasingly dependent on advanced code generation tools.

The overall methodology (the paper's Figure 1) combines several diagnostic sources:

• Hand-written directed diagnostics developed by members of the DVT team, including architectural (AVP), microarchitectural (MVP), and implementation (IVP) verification programs that set up and check conditions deemed interesting by the developer of each test.
• Advanced pseudorandom code generators that produce long instruction sequences.
• Tool-generated diagnostics from heuristic-based engines (and from real-world applications, in the case of multi-processor testing).

Diagnostics are simulated against both an RTL simulator and an architectural simulator; the resulting traces are compared by an architectural comparator (e.g., refdif) to detect mismatches that indicate a flaw in the implementation.

Categories of code generation tools

The paper divides code generation tools into three major categories:

• User-assisting tools — simplify and automate tedious tasks such as the permutation, iteration, and interleaving of existing instruction sequences into new sequences with interesting properties. They make the generation of diagnostics for known cases easier and less time-consuming.
• Pseudorandom code generators — focus on producing long sequences of legal instructions, assuming that the random interaction of these instructions will produce conditions rarely created by compiler-generated code or conceived by a programmer. The paper notes that they usually produce code of poor quality.
• Heuristic-based code generators — combine user-provided attributes and properties with knowledge of the architecture and of the design to produce algorithms that target the most complicated features of the design. They generate code of high quality by intelligently selecting instructions whose execution will create the proper conditions for an interesting case, which has not been previously covered, to arise.

Specific tools

SBVer (Store Buffer Verifier)

SBVer is a code generator that focuses on exercising the external interface and the cache management units of the microprocessor. Knowledge about the design of the primary and secondary caches, the various address spaces, and the memory management unit is built into the tool.

Theo

Theo is a sophisticated heuristic-based code generator. It is based on the idea that focusing on instruction sequences to which a particular implementation may be sensitive can reduce the number of test cases examined and improve the quality of the generated verification code.

• Templates. Users provide templates that define sequences of instructions representing "constraints." Templates may use symbolic notation for operands, symbolic names for registers, and symbolic instruction class names. This lets users focus on developing sequences for their own area of interest while Theo's engine searches for their "optimal" placement that satisfies the specified constraints.
• Goal. A typical hand-written diagnostic only stresses a particular unit while other sections of the microprocessor remain idle; Theo attempts to combine templates so that all units of the microprocessor are active simultaneously.
• Code generation process:
  1. Code generation starts with an uninstantiated Intermediate Code Representation (ICR) in which each element is a placeholder for an instruction with no particular attribute or property.
  2. Theo repeatedly selects a user-provided template and applies it to the ICR, transferring the template's instruction sequence, properties, and constraints into the ICR.
  3. The template placement algorithm avoids placing templates one after another. Instead, it strives to achieve overlap between templates while maintaining the requirements of each template. Overlap is checked via subset properties, constraint solving, and temporary unification; if all resource requirements are met, the unification becomes permanent. Successive application of templates to the ICR results in further refinement and growth of the code.
  4. Template placement stops when the code size requirement is met.
  5. Theo assigns actual instructions for any instruction-class references that remain in the ICR.
  6. Several managers — the register allocation manager, address manager, branch manager, operand manager, and external event manager — allocate resources and insert condition setups.
  7. The ICR is finally translated into assembly code.

The various managers encapsulate heuristic and formal algorithms that may be applied across the entire code stream and can be tuned with user biasing. The overlap-based approach has the unique property of creating new test sequences from previously independent blocks that now interact with each other, while still maintaining the sequence and conditions represented by each template.

MPAV (Multi-Processor Application Verifier)

MPAV is a code generation and execution environment for multiprocessor test programs. Real-world parallel applications — including the SPLASH-2 benchmarks, as well as chaotic algorithms and branch-and-bound algorithms — are ported onto this environment. To incorporate a new application, the user only needs to write three "interface functions": two perform the initializations of the data structures of the parallel program, and the third provides the environment with the "starting points" of the parallel program's execution. MPAV can also incorporate sequential applications, such as diagnostics programs created by other code generation tools. An X-based graphical user interface lets the user select the applications to be included in a particular execution, set the corresponding input parameters, and then compile and execute the resulting suite.

Analysis and feedback (the diagnostic database)

Because code generation tools tend to create a large number of lengthy diagnostic programs, and because only a limited number of them can be simulated daily on the (expensive) RTL model, the run-time behavior of diagnostics is analyzed systematically and automatically. Analysis code is executed on the trace file produced by simulation; results are expressed as a set of values for a prespecified, common set of attributes for all diagnostics. Example attributes include the number of instructions executed, the number of cache hits and misses, the lengths of various queues in the microprocessor, and exception counts. The paper's figure shows an example with attributes such as Author, ICount (e.g., 709), Immediate (e.g., 457), Arithmetic (e.g., 44), Exception (e.g., 4), CacheError (e.g., 1), and ExtInt (e.g., 3).

The paper introduces the Ans tool, which compresses this information into a highly efficient, object-based diagnostic database (referred to in the paper as ODDB or DDB). Ans is a general tool designed to handle any object-based collection of data; it both modifies the database and queries it to retrieve a set of objects (diagnostics) that satisfy a given set of criteria, expressed as equalities or inequalities on attribute values. For example, the query

((ICount <= 2000) && (FP Exception >= 10))

would select all diagnostics currently stored in the database with fewer than 2000 instructions and at least 10 floating-point exceptions.

Other profiler applications built on the same analysis pipeline include state coverage and comparison of traces. The analysis results stored in the diagnostic database are subsequently fed back to the code generation tools to improve both the quality of the generated code and the effectiveness and efficiency of the generators themselves. Two motivations are given: the pseudorandom nature of the code generators makes such analysis extremely useful for covering specific sets of interesting cases in depth, and the limited daily simulation capacity makes it important to focus the generated set on diagnostics most likely to be useful.

Flaw isolation: self-checking vs. trace comparison

The paper contrasts two approaches to isolating a design flaw.

• Self-checking code. The test program sets up a combination of conditions and then checks whether the RTL model reacted correctly. However, the state-compare instruction sequence is usually intrusive at the RTL level, coarse-grained and therefore less accurate, consumes precious simulation cycles, and may burden the code generation tool by requiring it to maintain an extensive amount of state.
• Non-intrusive trace comparison. The trace produced by simulating the diagnostic on the RTL model is compared with the trace produced by an architectural reference model. This frees the diagnostic from continuously checking the reactions of the design under test, is more accurate, allows a more powerful comparison process to be employed, and relieves the code generation tool from computing the results of all the instructions it generates. A powerful X-based graphical environment that exploits the information provided by the architectural comparator can then be used to debug the identified error.

Takeaway

Across the provided evidence, code generation is a unifying term for several activities that produce executable code or executable test programs from higher-level inputs:

• In compilers, code generation is the back-end stage of instruction selection, scheduling, resource assignment, and assembly, driven by rewrite rules that are increasingly being synthesized automatically from the architecture's RTL using SMT solvers (as in the DDM+22 paper).
• In LLM-based software development, code generation turns natural-language or formal specifications into source code, and the emerging verifiable variant additionally requires the model to produce a formal specification and a machine-checkable proof of code-specification alignment (VERINA). General-purpose LLM code generation can also be guided by structural constraints on the target language (GAP-Gen's Syntax-Flow and Variable-Flow over Python).
• In functional hardware verification, code generation is a tool-assisted, sometimes heuristic, and database-instrumented discipline for producing diagnostic instruction sequences that stress high-performance microprocessors, exemplified by SBVer, Theo, and MPAV in the 1996 DAC methodology.

These three contexts share a common theme: pushing more of the burden of producing correct, well-targeted code onto automated or semi-automated tooling, and using analysis (formal or empirical) to feed back into the generators themselves.