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$

closed as unclear what you're asking by R B, Kristoffer Arnsfelt Hansen, David Eppstein, Jeffε, András Salamon Dec 16 '14 at 20:45

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 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.