code generation
ConceptIn the provided evidence, code generation refers to the automated or semi-automated production of executable code (or test programs) from higher-level inputs, spanning at least three contexts: (1) compiler back-end code generation, in which instruction-selection rewrite rules translate an IR to a target ISA and may be synthesized from the architecture's RTL using SMT solvers; (2) LLM-based code generation, where natural-language descriptions or formal specifications are turned into code, optionally paired with specifications and machine-checkable proofs; and (3) functional-verification code generation, where tools produce diagnostic instruction sequences that drive simulation-based verification of high-performance microprocessors.
First seen 6/2/2026
Last seen 7/3/2026
Evidence 10 chunks
Wiki v3
WIKI
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.)
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
11 connectionsCode generation is used as a primary means of functional verification of microprocessors.
The diagnostic database is used to improve code generation tools.
Code generation employs pseudorandom methods as one approach.
Code generation employs heuristic-based methods as one approach.
The paper is motivated by and contributes to the code generation stage of compilers.
DVT teams increasingly depend on advanced code generation tools for functional verification.
Retargetable code generation is a specific form of code generation.
The paper focuses on code generation tools for microprocessor verification.
Code generation includes user-assisting tools as one category.
Intermediate Code Representation is an intermediate step in Theo's code generation pipeline.
AVPGEN is mentioned as a related test generator for architecture verification.
CITATIONS
15 sources15 citations — click to expand
[1] Code generation in a compiler is the back-end stage involving instruction selection, scheduling, resource assignment, and assembly, driven by rewrite rules that are dependent on the target ISA and usually constructed manually. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[2] Every new ISA must be accompanied by a set of rewrite rules that describe how to transform a compiler's IR to the ISA, and crafting these rules is a labor-intensive task. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[3] The DDM+22 paper synthesizes instruction-selection rewrite rules from an architecture's RTL by constructing first-order logic queries whose solutions, obtained via an SMT solver, represent the rewrite rules, and proposes a methodology for abstracting complex operations (e.g., floating-point) that previous SMT-based approaches could not model efficiently. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[4] Contributions of the DDM+22 paper include formalization of rewrite-rule correctness criteria, support for parametric rewrite rules, abstraction of complex operations, and an efficient SMT-based encoding for the synthesis problem. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[5] The DDM+22 authors synthesized rewrite rules from CoreIR to a family of CGRAs and from WebAssembly to various RISC-V architectures (including floating-point extensions) in seconds, and synthesized short multi-instruction sequences for pseudo-operations (documented or not) in at most 90 seconds. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[6] RISC-V does not include equals/not-equals instructions but documents pseudo-operations like (x - y) < 1 for unsigned less-than, and undocumented two-instruction sequences can implement less-than-or-equals and greater-than-or-equals via (y < x) ^ 1 and (x < y) ^ 1 respectively. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[7] GAP-Gen is a guided automatic Python code generation method based on Python syntactic and semantic constraints, introducing Syntax-Flow (a simplified AST) and Variable-Flow (which abstracts variable/function names), and fine-tunes T5 and CodeT5 on CodeSearchNet, CodeSearchNet AdvTest, and the Code-Docstring Corpus from EdinburghNLP, achieving better results on automatic Python code generation than previous works. GAP-Gen: Guided Automatic Python Code Generation
[8] VERINA defines 'verifiable code generation' as the joint generation of code, specifications, and proofs of code-specification alignment, and is a 189-task Lean benchmark with reference implementations, formal specifications, and extensive test suites. VERINA: Benchmarking Verifiable Code Generation
[9] On VERINA, OpenAI o3 achieves 72.6% code correctness, 52.3% specification soundness and completeness, and only 4.9% proof success rate, underscoring the need for improving LLM-based theorem provers in verification domains. VERINA: Benchmarking Verifiable Code Generation
[10] Functional verification aims to ensure the RTL model exhibits the same behavior as an architectural simulator when executing the same instruction sequence, and code generation tools (user-assisting, pseudorandom, heuristic-based) are central to this methodology. Code Generation and Analysis for the Functional Verification of Microprocessors
[11] SBVer is a code generator that exercises the external interface and cache management units of the microprocessor, with built-in knowledge of primary/secondary caches, address spaces, and the memory management unit. Code Generation and Analysis for the Functional Verification of Microprocessors
[12] Theo is a heuristic-based code generator that uses templates (with symbolic operands, register names, and instruction-class names), an uninstantiated Intermediate Code Representation (ICR), and a template placement algorithm that overlaps templates via subset properties, constraint solving, and temporary unification, with managers for register allocation, address, branch, operand, and external events. Code Generation and Analysis for the Functional Verification of Microprocessors
[13] MPAV is a code generation and execution environment for multiprocessor test programs that runs real-world parallel applications (SPLASH-2, chaotic algorithms, branch-and-bound) and sequential diagnostics from other code generation tools, using three user-supplied interface functions and an X-based GUI. Code Generation and Analysis for the Functional Verification of Microprocessors
[14] The Ans tool compresses run-time attribute data (e.g., ICount, FP Exception, CacheError, ExtInt) into an object-based diagnostic database (ODDB/DDB) supporting queries such as ((ICount <= 2000) && (FP Exception >= 10)), and the resulting metrics are fed back to the code generation tools to improve diagnostic quality and generator effectiveness. Code Generation and Analysis for the Functional Verification of Microprocessors
[15] Trace comparison between the RTL simulator and an architectural simulator using a comparator (e.g., refdif) is preferred over self-checking diagnostics because it is non-intrusive, more accurate, more powerful, and relieves the code generator from computing expected results. Code Generation and Analysis for the Functional Verification of Microprocessors