Here is my latest project.
InFormal connects Icarus Verilog to NuSMV for formal verification (aka. assertion based verification).
As a first release, it's a bit rough around the edges, but it works surprisingly well. InFormal has already caught real bugs in real designs. Just flip the "-a" switch for automatic assertions.
http://www.confluent.org/wiki/doku.php?id=informal:main
Enjoy!
-Tom
