gEDA-user: Re: [nusmv-users] if there are tools that convert verilog or VHDL to NuSMV?

[Tom Hawkins <tom@launchbird.com>]

On Friday 12 March 2004 11:52 pm, Shengyu Shen wrote:
> Hi everyone
> 
> I want to convert some of my large verilog file to NuSMV, so any
> tools that can do this?

I've looked into this.  An option is to use the frontend of either 
Icarus Verilog or Verilator, then write a NuSMV code generator on the 
backend.  Actually I would rather have Icarus or Verilator generate a 
netlists in XML; it would make it easier for developing custom tools 
around the Verilog language. 

For those on the geda list, NuSMV is an open source symbolic model 
checker used for formal verification.  (Is equivalence checking a 
special case of model checking?)  http://nusmv.irst.itc.it/

BTW, Confluence is a declarative functional programming language for 
synchronous reactive system design, e.g. digital logic.  From one 
source it emits Verilog, VHDL, C, XML, and NuSMV.  And just this week 
I release it as open source (GPL/LGPL).

Regards,
Tom

-- 
Tom Hawkins
Launchbird Design Systems, Inc.
952-200-3790
http://www.launchbird.com/