This is the supplementary materials associated to the "Fe-Si : Formal verification of hardware synthesis paper" It contains two directories. - src contains the sources of the compiler - examples contains the various examples discussed in the paper, as well as the prototype OCaml back-end to verilog. Each of this directory contains a README file with more informations. Running [make] builds the whole development. In the examples directory, running [make demo] generates examples cores.