Aria-HDL ^(WIP)

FPGA meta-compiler — from DSL to silicon, with formal proofs.

---

A hardware description language and compiler that generates synthesizable RTL, formal verification proofs, and GPU emulation kernels from a single source.

Built for systolic arrays, DNN inference, networking offload (DPDK/Virtual Ethernet), and cryptographic accelerators.

What It Does

                        ┌──→ Verilog ──→ Yosys / Vivado ──→ bitstream
                        ├──→ VHDL ──→ NVC / GHDL ──→ simulation
Aria-HDL source (.ahdl) ├──→ Verilator bundle ──→ C++ co-simulation
         │              ├──→ SVA / PSL + .sby ──→ SymbiYosys ──→ proofs
         ↓              ├──→ Lean 4 ──→ proof obligations
     Compiler IR        ├──→ CUDA kernel ──→ GPU semantic emulation
         │              ├──→ Metal shader ──→ Apple Silicon emulation
         │              ├──→ OpenCL kernel ──→ cross-vendor emulation
         │              └──→ JSON resource report ──→ design space exploration
         │
         └──→ Optimization: retiming, C-slowing, CDC enforcement, pipeline balancing

10 Backends

Backend	CLI Flag	Output
Verilog	--emit-verilog	Synthesizable Verilog with Memory, Instance, ApproxUnit ROM
VHDL	--emit-vhdl	IEEE 1076-2008, 100% IrExpr coverage
Verilator	--emit-verilator	Verilog + Makefile + C++ testbench + C API header
Formal	--emit-sby	SVA/PSL assertions + SymbiYosys config
Lean 4	--emit-lean4	Proof obligations with struct/enum type definitions
CUDA	--emit-cuda	GPU kernel with register state arrays
Metal	--emit-metal	Apple Silicon MSL compute shader
OpenCL	--emit-opencl	Cross-vendor GPU kernel
Resource	--resource-report	JSON: per-module LUT/reg/DSP/BRAM + approx Pareto front
IR dump	--emit-ir	Internal representation for debugging

DSL Features

Hardware Primitives module — combinational & sequential pipeline with |> stage boundaries systolic arrays with PE grids stream<T> with flow control fifo<depth=N> with CDC support approx() LUT-based function approximation	Type System int<N>, uint<N> — arbitrary width fix<W,I> — fixed-point fp32, fp16, bf16, fp8e4m3 bits<N> — raw bitvectors struct, enum (tagged unions) mx<T,N> — microscaling blocks
Formal Verification assert, assume, cover inline always, never, eventually temporal SVA / PSL auto-generation Lean 4 proof extraction SymbiYosys .sby config	Compiler Passes Type checking + width inference CDC enforcement (hard error) Retiming + critical path analysis C-slowing (throughput scaling) Pipeline latency balancing Resource estimation + Pareto DSE

Quick Start

# Build
cargo build --release

# Parse and emit Verilog
cargo run -- --emit-verilog examples/blinker.ahdl

# Get resource estimates (JSON for coding agents)
cargo run -- --resource-report examples/resource_demo.ahdl

# Generate Verilator co-simulation bundle
cargo run -- --emit-verilator examples/blinker.ahdl

# Formal verification bundle
cargo run -- --emit-sby examples/alu.ahdl

# GPU semantic emulation
cargo run -- --emit-cuda examples/blinker.ahdl
cargo run -- --emit-metal examples/blinker.ahdl
cargo run -- --emit-opencl examples/blinker.ahdl

Resource Estimation

The --resource-report flag outputs JSON that coding agents can consume:

{
  "module": "resource_demo",
  "total_luts": 320,
  "total_regs": 32,
  "total_dsps": 1,
  "total_bram_bits": 0,
  "breakdown": [
    {"name": "product", "kind": "wire", "luts": 256, "dsps": 1},
    {"name": "accumulator", "kind": "register", "luts": 48, "regs": 32},
    {"name": "overflow", "kind": "wire", "luts": 16}
  ],
  "approx_alternatives": []
}

For approx() blocks, enumerates Pareto-optimal alternatives meeting the error constraint.

Examples

Example	What it demonstrates
blinker.ahdl	LED blinker — var, when, @clock_freq
alu.ahdl	ALU — enum, match, struct, formal assert/cover
cpu8051.ahdl	8-bit CPU — complex match, bitwise ops
crypto.ahdl	Modular arithmetic — wide integers, formal proofs
dnn_inference.ahdl	Matrix multiply — systolic array, INT8 MACs
tcp_ip.ahdl	TCP checksum — var, state machine, assert always
sigmoid_lut.ahdl	Activation function — piecewise linear approximation
resource_demo.ahdl	Resource estimation — multiply vs add cost comparison

Compilation Pipeline

Source (.ahdl)
    ↓ Lexer (80+ tokens)
    ↓ Parser (recursive descent, .method<N>() generics)
    ↓ AST
    ↓ Lowering (enum tag/payload, const folding, GenericCall)
    ↓ IR (Wire, Register, Memory, Fifo, PipelineReg, PE, ApproxUnit, Formal)
    ↓ Type Check (width propagation, ref validation)
    ↓ CDC Enforcement (hard error on cross-domain wires)
    ↓ Retiming Analysis (critical path, opportunity detection)
    ↓ Backend Emission (10 targets)
Output

Target Hardware

Tier	Board / Card	FPGA	Use Case
Dev	Tang Nano 9K	GW1NR-9C	Learning, small demos
Dev	iCEBreaker	iCE40UP5K	OSS toolchain, blinker
Dev	ULX3S	ECP5-85F	Serious OSS projects, Linux SoC
Accel	Alveo U50	UltraScale+	Best value accelerator (used ~$200)
Cloud	AWS F2	VU47P HBM	100 Gbps Virtual Ethernet, DPDK
Cloud	Azure NP	Stratix 10	Intel FPGA cloud

Design Decisions

Decision	Choice	Rationale
GPU emulation	Semantic only	Clock-level is non-goal; focus on rapid DSE
ONNX import	Full parser	Support arbitrary models
MX block types	First-class	Core for DNN inference
Multi-clock	Hard error	Require explicit CDC FIFO — safety first
PCIe emulation	DPI-C primary	Zero-overhead co-simulation
Resource control	Formal-aware	Tightening approx must not break proofs

Project Structure

src/
  lexer.rs, parser.rs, ast.rs     — Frontend (80+ tokens, recursive descent)
  ir/                              — Hardware IR (types, expr, module, formal)
  lowering.rs                      — AST → IR conversion
  typecheck.rs                     — Width propagation, validation
  verilog.rs, vhdl.rs              — HDL backends
  verilator.rs                     — Verilator co-sim bundle
  formal.rs                        — SVA/PSL + SymbiYosys
  lean4.rs                         — Lean 4 proof extraction
  gpu.rs, metal.rs, opencl.rs      — GPU semantic emulation
  resource.rs                      — Resource estimation + Pareto DSE
  approx.rs                        — LUT generation + error analysis
  passes/                          — Optimization (c_slow, retiming, balance, cdc)
examples/                          — 8 demo designs
tests/                             — 50 tests (32 unit + 18 integration)

Testing

cargo test                         # All 50 tests
cargo test test_resource           # Resource estimation only
cargo test --test integration      # Integration tests only

Dependencies

Pure Rust, no external dependencies. cargo build is all you need.

Specs & Docs

• SPECS.md — Full specification (10 sections)
• DSL_SYNTAX.md — Language syntax + EBNF grammar
• IR_DESIGN.md — Compiler IR architecture
• STATUS.md — Current implementation status
• TODOs.md — Roadmap and design decisions