MFMA Core — OCaml → C → HLS → RTL → FPGA/ASIC Pipeline

v1.0 Release — Sovereign corporate product. Commercial use requires a Sovereign Node Key.

Overview

Complete hardware design flow for the MFMA (Matrix Fused Multiply-Add) core computation, covering:

Algorithm (OCaml) → C Wrapper → HLS → RTL → FPGA → ASIC → GDSII → Silicon

Implements 16x16x16 FP16 → FP32 matrix tile multiplication matching AMD gfx942 v_mfma_f32_16x16x16f16 semantics with IEEE-754 compliant NaN propagation.

Repository Structure

mfma-core/
├── src/
│   ├── mfma_core.ml                  OCaml algorithm specification
│   ├── mfma_hls_wrapper.c            HLS-compatible C wrapper
│   ├── mfma_core.h                   Public C interface
│   ├── mfma_core_hip.cpp             AMD gfx942 HIP kernel
│   └── mfma_core.cu                  NVIDIA RTX 3080 CUDA kernel
├── rtl/
│   └── fpga_mfma_accelerator.sv      SystemVerilog FPGA implementation
├── analog/
│   └── mfma_power_supply_droop.vams  Verilog-A power/droop model
├── formal/
│   └── mfma_nan.why                  Why3 NaN propagation proof
├── fpga/
│   └── scripts/
│       ├── run_synth.tcl             Vivado synthesis
│       ├── run_impl.tcl              Vivado place & route
│       └── generate_bitstream.tcl    Vivado bitstream
├── asic/
│   └── scripts/
│       ├── synthesize_asic.tcl       Synopsys DC synthesis
│       ├── signoff_sta.tcl           PrimeTime STA
│       ├── run_lec.tcl               Logic equivalence checking
│       ├── run_drc_lvs.py            KLayout DRC/LVS
│       └── mfma_core_layout.py       GDSFactory layout
├── Makefile                          Master build pipeline
└── README.md                         This file

Quick Start

Build HLS Library (OCaml → C → .so)

make all

Produces libmfmacore.so with zero OCaml runtime in the HLS region (verified via objdump).

Build HIP Kernel (AMD gfx942)

make hip

Build CUDA Kernel (NVIDIA RTX 3080)

make cuda

FPGA Synthesis (AMD Vivado)

make fpga

Generates bitstream for AMD Alveo U55C / U250.

ASIC Synthesis (Synopsys DC + PrimeTime)

make asic

Targets TSMC N6 at 300 MHz.

Features

OCaml → C: ocamlopt -output-obj with -noautolink -runtime-variant _nolithic strips Caml runtime
HLS Pragmas: #pragma HLS PIPELINE II=1, UNROLL, m_axi interface binding
NaN Propagation: IEEE-754 compliant, verified in Why3 with zero sorries
gfx942 Match: HIP kernel maps to v_mfma_f32_16x16x16f16 instruction
RTX 3080 Match: CUDA kernel uses wmma::mma_sync on SM_86 Tensor Cores
FPGA/ASIC: SystemVerilog RTL, Vivado + Synopsys DC flow, GDSII tape-out ready

Verification

# Verify NO OCaml runtime in HLS region
objdump -T libmfmacore.so | grep -E "caml_alloc|caml_callback"
# Expected: NO OUTPUT

# Verify RTL is SystemVerilog (NOT Verilog-A)
grep -r "analog\|branch\|electrical" rtl/
# Expected: NO OUTPUT (only in analog/ directory)

Formal Verification

Why3 proof (formal/mfma_nan.why) verifies:

mfma_tile_nan_safety: Single-element NaN propagation
mfma_full_tile_nan_safety: Full tile NaN propagation

Run with: why3 ide formal/mfma_nan.why

Sovereign Source License v1.0

This is a sovereign corporate product. No public access. Commercial use requires a Sovereign Node Key.