CHERI-CVA6 FORMAL VERIFICATION TEMPLATE

This is a template for formal on cheri-cva6. It is a fork of the cap limited cheri-cva6 repo.

The formal infra is under verif/formal. It has a Makefile, a script to process filelists, a basic (minimal) configuration of CVA6, a verify.tcl file and a formal top.

To make a private fork of this template:

1. Make a new empty repo, with no README, LICENSE, .gitignore or anything else
2. Clone your empty repo and cd <repo>
3. Add this template repo as a remote: git remote add template https://github.com/OX-FV/cheri-cva6-fv-template
4. Pull it: git pull template
5. Set your main main to be the main of this template: git branch --force main template/main
6. Checkout main: git checkout main
7. Push your new main to github: git push origin main:main

Now you have a private fork of this repo on which you can work. I suggest you do the following:

1. Check this opens in Jasper by
   1. Cloning the subrepos for cache and whatnot: git submodule update --init --recursive
   2. cd verif/formal
   3. make jg This should open CVA6 in Jasper
2. Check out the initial configuration in verif/formal/formal_config_pkg.sv and see if you want to tweak it
3. Check out the assumptions in verif/formal/top/formal_top.sv and verif/formal/verify.tcl

Then start writing properties in verif/formal/top/formal_top.sv.

As your project grows you may wish to change the structure of things, which you are absolutely welcome to do.

I (Louis-Emile) will be happy to help either by email or, (if I did something wrong, which is likely), you can open an issue in this repo.

CVA6 RISC-V CPU

CVA6 is a 6-stage, single-issue, in-order CPU which implements the 64-bit RISC-V instruction set. It fully implements I, M, A and C extensions as specified in Volume I: User-Level ISA V 2.3 as well as the draft privilege extension 1.10. It implements three privilege levels M, S, U to fully support a Unix-like operating system. Furthermore, it is compliant to the draft external debug spec 0.13.

It has a configurable size, separate TLBs, a hardware PTW and branch-prediction (branch target buffer and branch history table). The primary design goal was on reducing critical path length.

The CVA6 core is part of a vivid ecosystem. In this document, we gather pointers to this ecosystem (building blocks, designs, partners...).

A performance model of CVA6 is available in the perf-model/ folder of this repository. It can be used to investigate performance-related micro-architecture changes.

Quick setup

The following instructions will allow you to compile and run a Verilator model of the CVA6 APU (which instantiates the CVA6 core) within the CVA6 APU testbench (corev_apu/tb).

Throughout all build and simulations scripts executions, you can use the environment variable NUM_JOBS to set the number of concurrent jobs launched by make:

• if left undefined, NUM_JOBS will default to 1, resulting in a sequential execution of make jobs;
• when setting NUM_JOBS to an explicit value, it is recommended not to exceed 2/3 of the total number of virtual cores available on your system.

1. Checkout the repository and initialize all submodules.

git clone https://github.com/openhwgroup/cva6.git
cd cva6
git submodule update --init --recursive

2. Install the GCC Toolchain build prerequisites then the toolchain itself.

⚠️ It is strongly recommended to use the toolchain built with the provided scripts.

3. Install cmake, version 3.14 or higher.

4. Set the RISCV environment variable.

export RISCV=/path/to/toolchain/installation/directory

5. Install help2man and device-tree-compiler packages.

For Debian-based Linux distributions, run :

sudo apt-get install help2man device-tree-compiler

6. Install the riscv-dv requirements:

pip3 install -r verif/sim/dv/requirements.txt

7. Run these commands to install a custom Spike and Verilator (i.e. these versions must be used to simulate the CVA6) and these tests suites.

# DV_SIMULATORS is detailed in the next section
export DV_SIMULATORS=veri-testharness,spike
bash verif/regress/smoke-tests.sh

Tutorials

• Running Simulations
• ASIC Implementation
• FPGA Implementation and running an OS
• Instruction Tracing

Directory Structure

The directory structure separates the CVA6 RISC-V CPU core from the CORE-V-APU FPGA Emulation Platform. Files, directories and submodules under cva6 are for the core only and should not have any dependencies on the APU. Files, directories and submodules under corev_apu are for the FPGA Emulation platform. The CVA6 core can be compiled stand-alone, and obviously the APU is dependent on the core.

The top-level directories of this repo:

• ci: Scriptware for CI.
• common: Source code used by both the CVA6 Core and the COREV APU. Subdirectories from here are local for common files that are hosted in this repo and submodules that are hosted in other repos.
• core: Source code for the CVA6 Core only. There should be no sources in this directory used to build anything other than the CVA6 core.
• corev_apu: Source code for the CVA6 APU, exclusive of the CVA6 core. There should be no sources in this directory used to build the CVA6 core.
• docs: Documentation.
• pd: Example and CI scripts to synthesis CVA6.
• util: General utility scriptware.
• vendor: Third-party IP maintained outside the repository.
• verif: Verification environment for the CVA6. The verification files shared with other cores are in the core-v-verif repository on GitHub. core-v-verif is defined as a cva6 submodule.

verif Directories

• bsp: board support package for test-programs compiled/assembled/linked for the CVA6. This BSP is used by both core testbench and uvmt_cva6 UVM verification environment.
• regress: scripts to install tools, test suites, CVA6 code and to execute tests
• sim: simulation environment (e.g. riscv-dv)
• tb: testbench module instancing the core
• tests: source of test cases and test lists

Contributing

We highly appreciate community contributions. To ease the work of reviewing contributions, please review CONTRIBUTING.

Contributions to the documentation (docs/ and tutorials/ directories) are very welcome as well.

If you find any problems or issues with CVA6 or the documentation, please check out the issue tracker and create a new issue if your problem is not yet tracked.
The CVA6 Kanban Board loosely tracks planned improvements.

Publication

If you use CVA6 in your academic work you can cite us:

CVA6 Publication

@article{zaruba2019cost,
   author={F. {Zaruba} and L. {Benini}},
   journal={IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
   title={The Cost of Application-Class Processing: Energy and Performance Analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI Technology},
   year={2019},
   volume={27},
   number={11},
   pages={2629-2640},
   doi={10.1109/TVLSI.2019.2926114},
   ISSN={1557-9999},
   month={Nov},
}

Acknowledgements

Check out the acknowledgements.