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.
$\begingroup$
$\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
Add a comment
|
$\begingroup$
$\endgroup$
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.
answered Oct 17 '14 at 15:16
$\begingroup$
$\endgroup$
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.
