A modified version of Coq that contains an extraction backend for the functional hardware description language CLaSH.
root
- .github
- checker
- clib
- config
- coqpp
- dev
- doc
- engine
- gramlib
- ide
- interp
- kernel
- lib
- library
- man
- parsing
- plugins
- pretyping
- printing
- proofs
- stm
- tactics
- test-suite
- theories
- tools
- topbin
- toplevel
- vernac
- .gitlab-ci.yml
- .merlin.in
- .ocamlinit
- CODE_OF_CONDUCT.md
- CONTRIBUTING.md
- CREDITS
- INSTALL.md
- LICENSE
- META.coq.in
- Makefile
- Makefile.build
- Makefile.checker
- Makefile.ci
- Makefile.common
- Makefile.dev
- Makefile.doc
- Makefile.dune
- Makefile.ide
- Makefile.install
- Makefile.vofiles
- README.md
- azure-pipelines.yml
- configure
- configure.ml
- coq-refman.opam
- coq.opam
- coqide-server.opam
- coqide.opam
- default.nix
- dune
- dune-project
- install.sh
- shell.nix
Coq with CLaSH support
This version of Coq extends the extraction backend to the functional hardware description language CLaSH. Currently, only clash-prelude-0.11 is supported.
In order to support finite data types in Coq, the CompCert Integer library needs to be installed as well. Note that CompCert models the finite integer types as dependent modules. This causes the extraction backend to extract all functions and data types inside of this modul as well. However, this is no problem in the synthesizing process as the these functions and data types are optimized away by CLaSH as they are not linked to the extracted topEntity (sequential circuit) or root (combinational circuit) function of the specification. Take a look at the coq2clash examples after installing this version of Coq for further information.
Installation
See the Installation Guide for a detailed explanation of the tools that and libraries that have to be installed bevor the entire tool chain can be used.
Usage
In general, after following the installation guide, Coq can be started by:
$ /opt/coq/bin/coqide -R /opt/compcert/lib/compcert/coq compcertand CLaSH using the following command:
$ stack --resolver lts-9.21 exec clashiThe library coq2clash contains examples how combinational and synchronous sequential are described.