From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id C36D6D45F for ; Sat, 5 Nov 2005 18:34:52 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jA5HYpj4026450 for ; Sat, 5 Nov 2005 18:34:52 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA22821 for ; Sat, 5 Nov 2005 18:34:51 +0100 (MET) Received: from fuzzy.phpwebhosting.com (194.67-19-13.reverse.theplanet.com [67.19.13.194] (may be forged)) by nez-perce.inria.fr (8.13.0/8.13.0) with SMTP id jA5HYoFS026447 for ; Sat, 5 Nov 2005 18:34:50 +0100 Received: (qmail 5851 invoked from network); 5 Nov 2005 17:34:40 -0000 Received: from unknown (HELO [192.168.0.4]) (24.163.160.87) by 194.67-19-13.reverse.theplanet.com with (DHE-RSA-AES256-SHA encrypted) SMTP; Sat, 05 Nov 2005 12:34:40 -0500 Message-ID: <436CF6E4.8060307@confluent.org> Date: Sat, 05 Nov 2005 12:16:04 -0600 From: Tom Hawkins User-Agent: Mozilla Thunderbird 1.0 (X11/20050115) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Ray Heasman , cf-user Mailing List , caml-list@inria.fr Subject: Re: [cf-user] HDCaml 0.2.0 References: <436BA7D3.5080305@confluent.org> <1131138146.26370.11.camel@maze.mythral.org> In-Reply-To: <1131138146.26370.11.camel@maze.mythral.org> X-Enigmail-Version: 0.89.5.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 436CED3B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 436CED3A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ocaml:01 bug:01 api:01 ocaml:01 ocaml's:01 ocaml's:01 compiler:01 haskell:01 compiler:01 ocamlc:01 debugger:01 ocamldebug:01 ocamlprof:01 ocamldoc:01 transforming:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=FORGED_RCVD_HELO autolearn=disabled version=3.0.3 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 > > > >