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 D84E8BC62 for ; Fri, 16 Sep 2005 20:38:30 +0200 (CEST) Received: from postman.medtronic.com (postman.medtronic.COM [144.15.157.121]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j8GIcTCY015102 for ; Fri, 16 Sep 2005 20:38:30 +0200 Received: from bishop.pace.medtronic.COM (localhost [127.0.0.1]) by postman.medtronic.com (8.12.9/8.12.9) with ESMTP id j8GIcPsf015538 for ; Fri, 16 Sep 2005 13:38:25 -0500 (CDT) Received: from pace.medtronic.com. (nenya.pace.medtronic.COM [144.15.20.58]) by bishop.pace.medtronic.COM (8.9.1b+Sun/8.9.1) with ESMTP id NAA26506 for ; Fri, 16 Sep 2005 13:38:32 -0500 (CDT) Received: from [127.0.0.1] (IDENT:U2FsdGVkX1+eq7INhDUqRjv8O3lLCWXDmHOZug2k0Oc@localhost [127.0.0.1]) by pace.medtronic.com. (8.12.11/8.12.11) with ESMTP id j8GIcO4D002669 for ; Fri, 16 Sep 2005 13:38:24 -0500 Message-ID: <432B1120.9050909@confluent.org> Date: Fri, 16 Sep 2005 13:38:24 -0500 From: Tom Hawkins User-Agent: Mozilla Thunderbird 1.0 (X11/20041206) X-Accept-Language: en-us, en MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: HDCaml 0.1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 432B1125.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ocaml:01 assertion:01 synchronous:01 api:01 api:01 structures:01 hierarchical:02 functional:02 limitations:02 black:96 library:03 describing:03 structure:04 regs:04 hol:05 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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