koika
koika copied to clipboard
mit-plv
A core language for rule-based hardware design 🦑
Dear @cpitclaudel , We are trying out Koika to run part of an operating system on an FPGA. In a test case (a.k.a. `Example`) we are using `tc_compute` and `interpret_action`...
I noticed that the `getFields` function of the RISC-V example often gets called just to get the value of a single field (with calls along the line of `let funct3...
Hi, I'm new to coq and I am facing a few issues with understanding the code `MultiplierCorrectness.v`. I could understand till the lemma `mul_to_partial_mul`. I don't understand what the rest...
`valid_rs1` and `valid_rs2` are never read in the RISC-V example. Making sure that the values really correspond to `rs1` or `rs2` instead of stalling whenever at least one of them...
When synthesizing the RV32E example with the `unit/led` program on my TinyFPGA BX, the LED stays off. On the other hand, Cuttlesim and Verilator both behave as I expect them...
Perhaps not conventional usage but currently `unit_t`/`bits_t 0` sized input from an external function generates invalid Verilog. e.g. ~~~coq Definition Sigma (fn: ext_fn_t) := match fn with | f1 =>...
I'm interested in learning more about the upcoming module system. What are its main design objectives and how far along is it in its development? I also have one use...
Most of the proofs of the lemmas defined in the file `examples/rv/MultiplierCorrectness.v` do not pass. I did not check them all individually, but most of them seem to be outdated....
I get the following error when I attempt to compile `examples/cosimulation.v` : ``` /usr/bin/ld: blackbox.obj_dir.opt/verilated.o: in function `VerilatedContext::threadPoolp()': verilated.cpp:(.text+0x3212): undefined reference to `VlThreadPool::VlThreadPool(VerilatedContext*, unsigned int)' collect2: error: ld returned 1...
This PR brings: - Code updates to support Coq 8.18 and OCaml 8.14 - Tool chain rewrite to use Dune 3 instead of Make - Nix flake for stable development...
