<commit_before># Cava: Lava-style circuits in Coq

This is a work in progress attempt to encode Lava-style gate-level circuit
descriptions in Coq for circuit specification, formal verification and
extraction into VHDL or SystemVerilog for implementation on FPGAs. The code
is currently very experimental and in constant flux.

Please see the [contributing guide](CONTRIBUTING.md) for how to submit push
requests.

## Pre-requisites

### Nix

If you have the [Nix package manager](https://nixos.org/nix/) installed, you can
simply run `nix-shell` from the `oak-hardware/cava` directory. Coq, Haskell, and
Icarus Verilog will then be available in your `$PATH`.

### Non-Nix

Please install the following components:

* The [Coq proof assistant](https://coq.inria.fr/) version 8.9.2 or later
* The [coq-ext-lib](https://github.com/coq-community/coq-ext-lib) library for Coq.
* The [GHC Haskell compiler](https://www.haskell.org/ghc/) version 8.6.5 or later
* The [Icarus Verilog](http://iverilog.icarus.com/) circuit simulator version
  11.0 or later. GitHub link:
  [https://github.com/steveicarus/iverilog](https://github.com/steveicarus/iverilog)<commit_msg>Be precise about exactly which version of Coq is required: 8.11.0<commit_after># Cava: Lava-style circuits in Coq

This is a work in progress attempt to encode Lava-style gate-level circuit
descriptions in Coq for circuit specification, formal verification and
extraction into VHDL or SystemVerilog for implementation on FPGAs. The code
is currently very experimental and in constant flux.

Please see the [contributing guide](CONTRIBUTING.md) for how to submit push
requests.

## Pre-requisites

### Nix

If you have the [Nix package manager](https://nixos.org/nix/) installed, you can
simply run `nix-shell` from the `oak-hardware/cava` directory. Coq, Haskell, and
Icarus Verilog will then be available in your `$PATH`.

### Non-Nix

Please install the following components:

* The [Coq proof assistant](https://coq.inria.fr/) version 8.11.0.
* The [coq-ext-lib](https://github.com/coq-community/coq-ext-lib) library for Coq.
* The [GHC Haskell compiler](https://www.haskell.org/ghc/) version 8.6.5 or later
* The [Icarus Verilog](http://iverilog.icarus.com/) circuit simulator version
  11.0 or later. GitHub link:
  [https://github.com/steveicarus/iverilog](https://github.com/steveicarus/iverilog)
{'fraction_non_alphanumeric': 0.10927573062261753, 'fraction_numerical': 0.009741634900465904, 'mean_word_length': 4.544600938967136, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 12, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1300716', 'n_tokens_mistral': 793, 'n_tokens_neox': 744, 'n_words': 261}