[LLVMdev] VHDL to promela

Nuno Lopes nunoplopes at sapo.pt
Tue Dec 4 14:16:46 PST 2012


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


----- Original Message ----- 
From: "David Blubaugh" <davidblubaugh2000 at yahoo.com>
Sent: Tuesday, December 04, 2012 8:47 PM
Subject: [LLVMdev] VHDL to promela


To All,


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

David Blubaugh 




More information about the llvm-dev mailing list