Converting a Hardware description language to a functional programming language I am looking for some guidelines on converting a Hardware description language such as VHDL or Verilog to a Typed Language. The reason I want to do this is to formally verify a hardware whose behavioral description is written in HDL.
You could write an interpreter for VHDL or Verilog in e.g. Coq or Isabelle/HOL and then prove that translated hardware descriptions do the right thing. I know that people have done this, at least for fragments of the hardware description languages, see e.g. A Formal Executable Semantics of Verilog.  Companies like Intel or AMD formally verify (parts of) the design of their chips. Have a look at Roope Kaivola's work.