| Confluence | HDCaml | |
|---|---|---|
| Core Language | A pure functional language with a lenient application order and types checked at runtime. No support for file IO. | OCaml is a strict functional language with side-effects and a static type system. |
| Clocking | Multiple explicit clock domains, no clock manipulation. | One implicit clock domain per circuit. |
| Subcircuit Semantics | Systems created at every component instantiation. Systems inherit parent clock, reset, and enable. | Subcircuit partitions not restricted to function boundries. No implicit resetting or enabling. |
| Core Primitives | RTL logicals, arithmetics, registers, and blackboxes. No memories, assertions, or tristates. | RTL logicals, arithmetics, registers. PSL properties. No support for blackboxes yet. No memories or tristates. |
| Generated Outputs | Verilog, VHDL, C, NuSMV, JHDL | Verilog, PSL, C, SystemC |
| HDL Annotation | None, except for top-level ports. | Ports, sub circuits, and all interally named signals. |
| Verification Methods | Generated HDL and C simulation, NuSMV model checking. | Generated HDL, C, and SystemC simulation; simulation in OCaml; formal verification of Verilog+PSL. |