Mentions légales du service

Skip to content
Snippets Groups Projects
README.md 4.26 KiB
Newer Older
BATY Matthieu's avatar
BATY Matthieu committed
# heRVé
BATY Matthieu's avatar
BATY Matthieu committed
A Kôika implementation of a pipelined RISC-V processor with interruptions and exceptions.
BATY Matthieu's avatar
BATY Matthieu committed
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.
## Build Instructions
BATY Matthieu's avatar
BATY Matthieu committed
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
BATY Matthieu's avatar
BATY Matthieu committed
Tests have the following dependencies:
- A C++17 `gcc` compiler (tested on 13.3.0),
- [The Boost libraries](https://www.boost.org/) (tested with version 1.83),
BATY Matthieu's avatar
BATY Matthieu committed
- 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).

BATY Matthieu's avatar
BATY Matthieu committed
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.
BATY Matthieu's avatar
BATY Matthieu committed
Next, you can use:

- `make binaries` to build all the tests.
BATY Matthieu's avatar
BATY Matthieu committed
- `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.

BATY Matthieu's avatar
BATY Matthieu committed
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,
DESFRENE Gabriel's avatar
DESFRENE Gabriel committed
    - `make cuttlesim-debug` build a processor simulator that you can debug with `gdb`,
    - `make cuttlesim-tests` to run all the tests on the simulator.

BATY Matthieu's avatar
BATY Matthieu committed
    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`.
BATY Matthieu's avatar
BATY Matthieu committed
- 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).

BATY Matthieu's avatar
BATY Matthieu committed
Proof checking is done in two steps:
- Proof extraction with `make proofs-export`,
- Proof checking with `make proofs-check`.

## Synthesis Instructions

BATY Matthieu's avatar
BATY Matthieu committed
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).


BATY Matthieu's avatar
BATY Matthieu committed
Synthesis of the bitstream:
```sh
make core
make -C src/_objects/priv_rv.v/ top_ecpix5.bit MEM_NAME=...
```

BATY Matthieu's avatar
BATY Matthieu committed
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
```
BATY Matthieu's avatar
BATY Matthieu committed

Happy hacking !