I just started a framework for describing hardware structures in OCaml. 
  Given a functional hardware description, HDCaml will produce a Verilog 
netlist for verification and implementation.

HDCaml also has decent PSL support for assertion based verification.

Current Limitations:
   - Synchronous, single clock.
   - No black boxing.
   - Basic regs only.  No memories.
   - Flat netlisting.

Possible Future Directions:
   - Better clock control.
   - Hierarchical netlisting.
   - C, VHDL, NuSMV code generation.
   - Links to HOL Light.

Any recommendations on the API structure or library features would be 
appreciated.

-Tom



HDCaml Download:

   http://www.confluent.org/

API Docs:

   http://www.confluent.org/misc/hdcaml/Hdcaml.html