HDCaml is a hardware design and verification language embedded in OCaml.

With release 0.2.5, HDCaml now produces cycle and bit accurate C models 
for simulation.  In addition to the logic primitives, the C models also 
support basic assertions of the form:

   assertion "label" (always (prop (some_signal)));

The C models include a SystemC wrapper for integration into any SystemC 
environment.  The wrapper is currently untested, so feedback from any 
SystemC user is appreciated.  Thanks!

http://www.confluent.org/

-Tom