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.
This work on "HML" does the reverse - it compiles an ML-like hardware description language to VHDL - but it might offer some insights on how to relate constructs in these languages.