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