NutShell Formal Verification

This project is a case study using riscv-spec-core on Nutshell for formal verification.

NutShell (果壳)

NutShell is a processor developed by the OSCPU (Open Source Chip Project by University) team. Currently, it supports riscv64/32. More information about NutShell see its GitHub repo.

Run Verification Directly

Install Dependency

Install btormc:

git clone https://github.com/Boolector/boolector.git
cd boolector
./contrib/setup-lingeling.sh
./contrib/setup-btor2tools.sh
./configure.sh && cd build && make -j$(nproc)
sudo make install
cd ../..

Initialize This Project

git clone https://github.com/iscas-tis/nutshell-fv
cd nutshell-fv
git submodule update --init --recursive

Run Verification

In this project, run:

mill chiselModule.test.testOnly formal.NutCoreFormalSpec

This will run the test case formal.NutCoreFormalSpec, which transforms NutCore (core computing unit) with assertions and SpecCore in riscv-spec-core to a transaction system and then passes it to the formal verification backend.

Modifications On NutShell

Search Formal in source code to see the main modifications.