0
$\begingroup$

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.

$\endgroup$
5
  • 7
    $\begingroup$ It might be easier to give a meaningful answer to your question if you give a bit of context. What are the goals of such a conversion? What properties should the conversion preserve? $\endgroup$ – Martin Berger Oct 15 '14 at 8:20
  • 3
    $\begingroup$ Look at the work of Koen Claessen on Lava or Geraint Jones on Ruby. $\endgroup$ – Dave Clarke Oct 15 '14 at 15:05
  • $\begingroup$ Thank you Dave. I am working along the lines of Lava and Ruby. $\endgroup$ – jhenry Oct 15 '14 at 21:40
  • $\begingroup$ Martin. My intention is to formally verify a hardware circuit and for that reason I want to convert HDL to a platform where I can use formal verification tools. $\endgroup$ – jhenry Oct 15 '14 at 21:42
  • 3
    $\begingroup$ Please edit your question so that people can understand what you are asking without reading comments. $\endgroup$ – Tsuyoshi Ito Oct 16 '14 at 23:38
3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.