FIRRTL is a language to describe an integrated circuit. It comes in a “high” and a “low” variant: the high variant looks like a simple programming language, while the low variant is quite close to a netlist (a graph of basic IC components like logic gates and their connections). Formal semantics for the low variant exist but the high FIRRTL semantics is given in English prose. I shall discuss ideas how to define formal semantics for high FIRRTL. We want to use this to formally verify that our compiler from high to low FIRRTL preserves the semantics; I shall also explain the current status of our compiler.