llvm dev - Dec 2012 - [LLVMdev] VHDL to promela

To All,
 
 
Has anyone worked with generating vhdl code to promela script for the spin model
checker??
 
David Blubaugh
 
 
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20121204/b76bd607/attachment.html>

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