OCaml All The Way Down

Hardware Design Approach

• The presentation details the design of FPGA hardware using the HardCAML Domain-Specific Language (DSL) within OCaml.
• The current demonstration utilizes a vendor-provided MicroBlaze soft CPU rather than a purely HardCAML-designed processor due to the scope of the demo.
• The backend toolchain relies on standard Xilinx FPGA place-and-route tools, as the presenter noted that managing the entire toolchain in-house is not currently feasible.
• The system integrates three primary hardware IP cores:
  • A DigilLED driver for the front LED strip (implemented in HardCAML).
  • An SPI core connected to a light sensor.
  • A CORDIC core for hardware-efficient calculation of trigonometric and hyperbolic functions using only additions and shifts.

FPGA Architecture and Resources

• Modern FPGAs consist of a grid of Logic Elements (LUTs) and registers, connected via local and global routing networks.
• LUTs are implemented using 16 static RAM cells (historically 4-input; modern devices typically use 6-input LUTs) to implement any Boolean function.
• Block RAMs are a critical resource, offering bandwidths in the terabit-per-second range when aggregated, enabling high-speed data processing.
• DSP blocks are hard silicon multipliers optimized for floating-point arithmetic and specific signal processing applications.
• Clocking resources (PLLs/DCMs) generate multiple phase-shifted and frequency-divided clocks to handle propagation delays across the chip.
• High-end FPGAs increasingly include "hard blocks" such as PCIe, Gigabit Ethernet, and embedded ARM cores (e.g., quad-core ARM running at 1.2 GHz).

RTL and Hardware Description Languages

• The industry standard remains VHDL, SystemVerilog, and increasingly C-based languages (SystemC, HLS), though the presenter notes these were originally conceived as documentation languages rather than design languages.
• Hardware description languages are event-driven; combinational logic updates on signal changes, while sequential logic (registers) updates on clock edges.
• Commercial simulators like ModelSim, VCS, and Riviera-PRO dominate, while the open-source landscape includes Icarus Verilog, GHDL, and Verilator (C++ converter).
• A significant gap exists in the open-source community regarding SystemVerilog support, which is now the standard for vendor IP.
• Advanced verification techniques include constrained random stimulus generation and temporal assertion-based property checking.
• Formal verification using SAT solvers allows proving circuit correctness for any input state (e.g., proving a 10-bit adder is correct by proving the negation is unsatisfiable).

HardCAML DSL Implementation

• HardCAML models hardware as a graph of nodes (registers, memories, muxes, arithmetic units) rather than a standard compiler AST.
• The language supports variable-width vectors, enabling self-adaptive designs where signal width can be queried at elaboration time.
• The API is strictly typed regarding signed/unsigned operations and signal widths, with errors caught at "elaboration" (graph construction) time.
• The always DSL constructs in HardCAML mimic Verilog always blocks to define state machines and guarded assignments.
• Memory structures are built from primitives (asynchronous read) with registers added to address/output ports to infer read-before-write or write-before-read behavior.
• HardCAML currently generates Verilog that is described as "entirely unreadable," creating challenges for debugging and timing analysis.

Software Stack and Embedded Execution

• The software runs on a MicroBlaze processor executing OCaml bytecode via the ZINC Abstract Machine interpreter.
• The build process involves cross-compiling the OCaml runtime, converting the program to bytecode, embedding the bytecode into a C array, and linking it with C stubs for the MicroBlaze environment.
• The current software footprint is large: base execution requires ~400KB, core libraries push it to ~700KB, and the full environment with the top-level interpreter reaches ~23MB.
• The OCaml top-level is functional on the FPGA, allowing interactive debugging and register manipulation via a USB-to-TCP bridge.
• Current limitations include the lack of native Unix file system support and networking (though an RJ45 interface exists), as well as the absence of a full Unix module implementation.

Demonstrations and Testing

• LED Control: Demonstrated Pulse Width Modulation (PWM) to create "breathing" LEDs and a "Cylon" effect using HardCAML for the driver logic.
• Sensors: A light sensor connected via SPI was used to display ambient light intensity on the LED strip, requiring averaging over ~500 samples to filter noise.
• Math: The CORDIC core was used to calculate and display cosine functions across the LED strip, handling phase reduction and quadrant symmetry in software.
• Concurrency: A demonstration utilized HardCaml step test bench and Async (OCaml) to run three independent tasks (strobe sequences) on the FPGA.
• Verification: The team uses cycle-accurate simulation and "waveform expect tests" for continuous integration, comparing actual waveforms against expected outputs.
• Formal Verification: HardCAML supports equivalence checking using SAT solvers and bounded model checking for sequential circuits.

Future Directions and Challenges

• The team plans to release an updated HardCAML version via Jane Street repositories, featuring improved testing infrastructure.
• Future work includes releasing the HardCaml step test bench and MicroBlaze simulator as separate packages.
• Long-term goals include developing a custom soft CPU designed entirely in HardCAML to eliminate dependency on vendor toolchains and C code.
• The team is investigating integration with BlueSpec-style atomic action modeling on top of HardCAML to improve architecture inference.
• Formal verification capabilities are being expanded, with recent integration of the Z3 SMT solver via OCaml bindings replacing older SAT solvers like MiniSat.