Newer
Older
A Kôika implementation of a pipelined RISC-V processor with interruptions and exceptions.
This design is based on [our fork of Kôika](https://gitlab.inria.fr/SUSHI-test/FMH/koika/).
The initial version of the processor is the work of Gabriel Desfrene.
This processor is based on the RISC-V _Kôika_ processor provided as a demonstration of the possibilities of this language.
Start by building and installing [our fork of Kôika](https://gitlab.inria.fr/SUSHI-test/FMH/koika/). Follow the instructions there first.
Then, running `make core` or `make` in the root directory builds the core in the Verilog file in `src/_objects/priv_rv/rv32.v`.
A pipeline schematic can be compiled with `make doc`. This target requires `latexmk`. The produced file is in `/src/doc/Pipeline.pdf`.
## Tests Instructions
- A C++17 `gcc` compiler (tested on 13.3.0),
- [The Boost libraries](https://www.boost.org/) (tested with version 1.83),
- A RISC-V compiler (you can use [this one](https://github.com/xpack-dev-tools/riscv-none-elf-gcc-xpack)),
- `bat`/`batcat`
- The [Verilator](https://github.com/verilator/verilator) suite (tested with version 5.024).
These simulations execute the processor, cycle by cycle, on custom programs found in the `src/test` directory.
To build the tests program, please adapt the `RISCVCC32` variable in the `Makefile` found in the `src/test` directory.
- `make binaries` to build all the tests.
- `make build-file FILE=test-prog` to build the test program `test-prog`. This should be a path relative the test directory without the file extension, example: `FILE=integ/tiny` is valid.
- `make dump-file FILE=test-prog` dumps the program on stdout with `objdump`.
When creating your own tests, you can append `-int` to your file name to add an interrupt manager or `-opt` to activate
compilation optimizations with the `-O2` flag.
Two simulations are available to test the processor:
- A high-level simulation with _cuttlesim_. The following commands are available:
- `make cuttlesim` to build the processor simulator,
- `make cuttlesim-trace` to build a processor simulator with debug output on stdout,
- `make cuttlesim-debug` build a processor simulator that you can debug with `gdb`,
- `make cuttlesim-tests` to run all the tests on the simulator.
You can use the following command to simulate on test programs:
- `make run-file FILE=test-prog STEPS=...` to simulate the processor on the program `test-prog`. The `STEPS` variable controls the number of cycle of the simulation,
- `make trace-file FILE=test-prog STEPS=...` to simulate and output the trace of the processor on the program `test-prog`,
- `make debug-file FILE=test-prog STEPS=...` to debug the `cuttlesim` simulator on the program `test-prog` with `gdb`.
- A low-level simulation with _Verilator_. The following commands are available:
- `make verilator` to build the processor simulator,
- `make verilator-tests` to run all the tests on the simulator.
More option are available on the `Makefile` in the `src/_objects/priv_rv`, use `make help` to describe them. The `NCYCLES` and `MEM_NAME` controls what file is simulated and for how long.
## Proof Instructions
To checks the proofs you will need the [z3](https://github.com/Z3Prover/z3) SMT solver (tested with version 4.13.0).
- Proof extraction with `make proofs-export`,
- Proof checking with `make proofs-check`.
## Synthesis Instructions
Synthesis can be done for various targets, see the `Makefile` in `src/_objects/priv_rv`. For synthesis on the ECPIX5 platform, you will need:
- [YoSys](https://github.com/YosysHQ/yosys) (tested with version 0.43),
- [nextpnr](https://github.com/YosysHQ/nextpnr) (tested with version 0.7),
- [Project Trellis](https://github.com/YosysHQ/prjtrellis) (tested with version 1.4),
- [openFPGALoader](https://github.com/trabucayre/openFPGALoader) (tested with version v0.12.0).
```sh
make core
make -C src/_objects/priv_rv.v/ top_ecpix5.bit MEM_NAME=...
```
The bitstream file is produced at `src/_objects/priv_rv.v/top_ecpix5.bit`. You can use the following command to flash the FPGA:
```sh
openFPGALoader -b ecpix5 src/_objects/priv_rv.v/top_ecpix5.bit
```