Architecture Formalization

Concept

Architecture formalization is the process of representing a target hardware architecture as a tuple of SMT formulas, enabling automated reasoning about instruction-level behavior for tasks such as instruction selection rewrite rule synthesis. Each architecture is parameterized by an instruction value that selects among possible operations on inputs and states.

First seen 6/8/2026

Last seen 6/8/2026

Evidence 3 chunks

Wiki v1

WIKI

Architecture Formalization

Overview

In the context of hardware compiler construction, architecture formalization refers to the representation of a target processor or hardware block as a logical structure suitable for automated reasoning. The approach is motivated by the need to avoid manually maintained Instruction Set Architecture (ISA) specifications, which are difficult to keep in sync with rapidly evolving Register-Transfer Level (RTL) designs and which typically fail to capture the instruction format or the instruction decode logic needed for an end-to-end correctness argument [bf650b47]. By formalizing architectures directly, one can reason about their behavior in many-sorted first-order logic and use an SMT solver to mechanically derive properties such as valid instruction selection rewrite rules [4499a813].

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT ← mentions 90% 2e

The paper formalizes architectures as SMT formula tuples.

LINKED ENTITIES

1 links

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT MENTIONS Extracted graph relationship

CITATIONS

10 sources

10 citations — click to expand

[1] An architecture is a circuit parameterized by a single architectural instruction value that indicates how other inputs and existing states are transformed into outputs and next states. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[2] Architectures are represented as tuples of SMT formulas of the form Arch(inst, y) = (Arch1(inst, y), …, Archn(inst, y)), with the instruction modeled as a variable inst of sort τ. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[3] Formalization proceeds in many-sorted logic with a set S of sort symbols and an infinite set of variables per sort; |= denotes the satisfiability relation. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[4] An 8-bit ALU with four operations can be encoded using nested ite expressions over a BV[2] operation selector and BV[8] operands, e.g., selecting between subtraction, addition, multiplication, and division. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[5] Architectures with states are modeled by including current state values as inputs and next-state values as outputs, with formulas Archn+i encoding the next-state function for the i-th state variable. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[6] Multiple architectures can be composed by concatenating instruction selectors and state vectors and rewiring outputs of one architecture into designated inputs of another via substitution. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[7] A simple state-free rewrite rule is a tuple (IR, Arch, instc) that is valid when ∀x. Arch(instc, x) = IR(x) is well-formed and T-valid; more general rules add a binding (bin, bout) so that validity is ∀x. bout(Arch(instc, bin(x))) = IR(x). Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[8] Using RTL directly avoids manual ISA specifications, which are hard to keep in sync with evolving designs and which typically omit the instruction format and decode logic needed for an end-to-end correctness argument; this is especially valuable during design space exploration. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[9] The framework's main contributions include formalizing correctness criteria for a general class of rewrite rules, supporting parametric rewrite rules, abstracting operations with unknown or complex semantics (e.g., floating-point), and an SMT-based methodology for encoding and solving the synthesis problem. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

[10] The approach has been used to synthesize rewrite rules from CoreIR to a family of CGRAs and from WebAssembly to RISC-V architectures (base ISA and extensions). Synthesizing Instruction Selection Rewrite Rules from RTL using SMT