VHDL to promela


To All,


Has anyone worked with generating vhdl code to promela script for the spin model checker??

David Blubaugh




|

I'm only aware of PinaVM, which includes a backend to translate LLVM IR to promela.
PinaVM, however, is designed to analyze System C, but I guess you can ignore the parts that are specific to SystemC; everything else is plain C++.

If you want to convert directly from VHDL, then probably LLVM is not an option, since LLVM doesn't have a front-end for VHDL, and it probably doesn't make sense to have one either.

Nuno