Re: [cf-user] HDCaml 0.2.0

[Tom Hawkins <tom@confluent.org>]

Hi Ray,

Ray Heasman wrote:
> Hi Tom,
> 
> Thanks for the update. It evokes a few questions.
> 
> On Fri, 2005-11-04 at 12:26 -0600, Tom Hawkins wrote:
> 
>>HDCaml is a hardware description language embedded in OCaml.  Given a 
>>digital design in HDCaml, the tools will output a synthesizable Verilog 
>>netlist with PSL assertions for verification.
> 
> 
> Is confluence still going to be around? I haven't used it for a few
> months, but I really liked it. I actually wrote useful stuff for work in
> it. I stuck with an older version though, because I needed a consistent
> environment.

It's not going to disappear, but I am no longer actively developing it. 
  However, I'm more than willing to fix the occasional bug.

> 
> 
>>Though HDCaml is still in early beta, 0.2 has undergone a major cleanup 
>>of the API.  All comments are welcome.  To download...
>>

> 
> I have no experience with ocaml, though I intend to play some day. Is
> there any reason I should use HDCaml instead of confluence? Also, I tend
> to prefer VHDL over verilog (I am a bondage-and-discipline programmer),

I think you just answered your own question.  Unlike Confluence, OCaml 
has an excellent type system that catches a vast majority of bugs at 
compile time.  OCaml's type system is far stronger than that of C++, 
Java, and even VHDL.  And unlike these languages, OCaml's compiler is 
smart enough to infer types automatically -- type declarations are 
usually optional.

OCaml and Haskell programmers have an expression: "Once it compiles, it 
usually just works!"

> so I am not overjoyed that HDCaml only does verilog.

The HDCaml Verilog generator is only 90 lines of code.  In time, HDCaml 
will write out VHDL, SystemC, and other popular netlist formats.  Maybe 
you would like to write the VHDL back-end?  There is no better way to 
learn a new language than writing a real application.

> 
> I'm interested if you have some sort of game plan in mind. I started
> losing the plot when you moved to the FNF and generating stuff for
> verification tools.   I have generally worked on small fry designs
> (largest has been 70000 gates) in a pretty informal FPGA environment. I
> like the idea of verification, but I feel you are so far ahead of me
> that I don't even understand what you are trying to do anymore. An
> overview would be very very interesting to me.

The real benefit of HDCaml is that it is embedded in a real [powerful] 
general purpose programming language.  Most of the development tools are 
already in place, including:

- Compiler (ocamlc)
- Interactive Interpreter (ocaml)
- Debugger (ocamldebug)
- Profiling (ocamlprof)
- Source Code Documentation Generator (ocamldoc)
- Standard Libraries (the basic data structures are all ready written)

The other benefit is, the language that describes hardware is the same 
language that can analyze and transform hardware descriptions.  What 
kind of analysis and transformations are possible?  Obviously, we need 
some netlist generators (transforming the intermediate circuit 
representation into VHDL).  Here are a few other examples:

- Custom Reports
   - How many flops, multipliers, and memories are in my design?
- Custom Lint Checks
   - Does my circuit have any combinational loops?
- Custom Optimizations
   - Remove all null effect logic in a circuit.
   - Replace register enables with clock-gating.
- Circuit Visualization
   - Writing the circuit to Graphviz dot.
- Manipulate the Design Hierarchy
   - Expand or collapse design levels.
   - Merge two asynchronous circuits.
- Rough timing estimation.

Most of these "plug-ins" are trivial, requiring only about 30-80 lines 
of OCaml.  We can take this a step further by starting to simulate and 
verify circuits within OCaml.  Here are some possibilities:

- Converting a circuit into a simulatable object.
- Stimulus generation.
   - Directed testing.
   - Constrained random.  (Possibly another OCaml embedded language?)
- Co-simulate with real firmware.  (OCaml can interface with C.)
- VCD generation.  (We all like to look at waveforms.)
- Model checking.
- Automated theorem proving.
   - HOL Light
   - MetaPRL

In short, you'll have a unified environment for design and verification.

-Tom


> Perhaps some homework
> reading material too, seeing as I don't have the time to actually dig
> into real code right now.
> 
> Thanks for your work so far. I really think confluence is an inspired
> idea.
> 
> Keep well,
> Ray
> 
> 
> 
>