<commit_before># Kami Experiments

This directory contains an attempt to use the [Kami](https://github.com/mit-plv/kami) system to specify a simple circuit and drive it through the point where we can generate a Verilog netlist which can be implemented and a Xilinx FPGA board and run.

The example we start with is a simple 4-bit counter [Counter.v](counter.v):
```
Require Import Kami.
Require Import Kami.Syntax.

Require Import Kami.Synthesize.
Require Import Ext.BSyntax.

Definition count := MethodSig ("counter" -- "count_value") (Bit 4) : Void.

Definition counter4 := MODULE {
    Register "counterReg" : Bit 4 <- $0

    with Rule "incrementAndOutput" :=
       Read val <- "counterReg";
       Write "counterReg" <- #val + ($1 :: Bit 4);
       (* Call count (#val); *)
       Retv

    with Method "count_value" () : (Bit 4) :=
       Read counterValue <- "counterReg";
       Ret #counterValue

  }.

Hint Unfold count : MethDefs.
Hint Unfold counter4 : ModuleDefs.<commit_msg>Fix name of counter Coq file<commit_after># Kami Experiments

This directory contains an attempt to use the [Kami](https://github.com/mit-plv/kami) system to specify a simple circuit and drive it through the point where we can generate a Verilog netlist which can be implemented and a Xilinx FPGA board and run.

The example we start with is a simple 4-bit counter [Counter.v](Counter.v):
```
Require Import Kami.
Require Import Kami.Syntax.

Require Import Kami.Synthesize.
Require Import Ext.BSyntax.

Definition count := MethodSig ("counter" -- "count_value") (Bit 4) : Void.

Definition counter4 := MODULE {
    Register "counterReg" : Bit 4 <- $0

    with Rule "incrementAndOutput" :=
       Read val <- "counterReg";
       Write "counterReg" <- #val + ($1 :: Bit 4);
       (* Call count (#val); *)
       Retv

    with Method "count_value" () : (Bit 4) :=
       Read counterValue <- "counterReg";
       Ret #counterValue

  }.

Hint Unfold count : MethDefs.
Hint Unfold counter4 : ModuleDefs.
{'fraction_non_alphanumeric': 0.10737581535373808, 'fraction_numerical': 0.009031610637230306, 'mean_word_length': 3.316017316017316, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 3, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, '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': '567164', 'n_tokens_mistral': 620, 'n_tokens_neox': 581, 'n_words': 234}