<p>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 href="http://fsl.cs.illinois.edu/index.php/A_Formal_Executable_Semantics_of_Verilog" rel="nofollow">A Formal Executable Semantics of Verilog</a>.  Companies like Intel or AMD formally verify (parts of) the design of their chips. Have a look at <a href="http://www.informatik.uni-trier.de/~ley/pers/hd/k/Kaivola:Roope" rel="nofollow">Roope Kaivola</a>'s work. </p>

CC BY-SA 3.0
2014-10-17T15:16:43.910Z
2014-10-17T15:16:43.910Z
Martin Berger
<p><a href="http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=486388&amp;tag=1" rel="nofollow">This work on "HML"</a> 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.</p>

CC BY-SA 3.0
2014-11-20T21:42:00.953Z
2014-11-20T21:42:00.953Z
Chris Martens
<p>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.  </p>

CC BY-SA 3.0
2014-10-15T08:20:46.077Z
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?
Martin Berger
CC BY-SA 3.0
2014-10-15T15:05:07.593Z
Look at the work of Koen Claessen on Lava or Geraint Jones on Ruby.
Dave Clarke
CC BY-SA 3.0
2014-10-15T21:40:27.837Z
Thank you Dave. I am working along the lines of Lava and Ruby.
jhenry
CC BY-SA 3.0
2014-10-15T21:42:34.030Z
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.
jhenry
CC BY-SA 3.0
2014-10-16T23:38:15.463Z
Please edit your question so that people can understand what you are asking without reading comments.
Tsuyoshi Ito
<pl.programming-languages>
Converting a Hardware description language to a functional programming language
jhenry
# Converting a Hardware description language to a functional programming language

(Asked by: username_0 on 2014-10-14)

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.

**Tags:** pl.programming-languages
> **Comments:**
> **username_1**: 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?  
> **username_2**: Look at the work of Koen Claessen on Lava or Geraint Jones on Ruby.  
> **username_0**: Thank you Dave. I am working along the lines of Lava and Ruby.  
> **username_0**: 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.  
> **username_3**: Please edit your question so that people can understand what you are asking without reading comments.  

---

## 2 answers

### Answer by username_1 on 2014-10-17. Score: 3

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](http://fsl.cs.illinois.edu/index.php/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](http://www.informatik.uni-trier.de/~ley/pers/hd/k/Kaivola:Roope)'s work.


---

### Answer by username_4 on 2014-11-20. Score: 2

[This work on "HML"](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=486388&tag=1) 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.


---

