Documentation
Fifteen pages in reading order. Start with the four background pages: they explain what a clock edge is, where the design came from, and what Rust does and does not check. Then the nine tool crates, bottom-up — bits, then the graph, then the two backends that read it.
Every page is a numbered walkthrough with the code samples transcribed from the crates themselves. Where something is a measured number, it is labelled as one, and where something is a known gap, it says so.
Background
How a circuit becomes a value
Combinational and sequential logic, clock edges, bit order, and what equivalence checking actually proves.
OCaml, and the idea of a hardware DSL
The three ways to write hardware, what a hardware construction language is, and which OCaml features carry weight.
Hardcaml, the design being ported
Signal.t, Reg_spec, wire and feedback, Cyclesim, ppx interfaces — and the three checks inherited verbatim.
Why Rust, honestly
What the type system does not check, where compile-time width checking was traded away, and what actually verifies the design.
Benchmarks, measured
Node counts, flops, bits of state and combinational depth for every design, derived from the IR rather than estimated.
The toolchain, bottom-up
Fixed-width bitvectors
ferrite-lithic-bitsRuntime-width integers over u64 words, with the width rules that make Verilog agree with you.
The graph
ferrite-lithic-irNodes, widths and dependencies. No behaviour, no types, no opinions about what hardware is.
The front end
ferrite-lithicDesign is an arena behind builders, and a Signal is a node id with a cached width.
The cycle simulator
ferrite-lithic-simCombinational within a cycle, sequential at the edge, and the edge is a real boundary.
The Verilog emitter
ferrite-lithic-rtlOne structural always block for the whole design, and a signature both backends agree on.
Ports by derive
ferrite-lithic-deriveA port list is a struct, and the derive reads the shape rather than a list of strings.
Waveform data
ferrite-lithic-waveCycle-indexed values you assert on directly, plus a VCD rendering for when you want eyes.
Verilator equivalence
ferrite-lithic-cosimTwo backends, one stimulus, compared cycle by cycle, with the first difference reported.
Step testbenches
ferrite-lithic-tbCoroutine testbenches where every await is one clock edge.
The corpus
ferrite-lithic-corpusTwenty-one real algorithms written the way hardware would want them, each checked three ways.
What the corpus found
ferrite-lithic-corpusNine defects, and one shape: a constant that looks right, builds a graph of exactly the right width, and means the opposite of what it says.