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

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.

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 ../..

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

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.

Search Formal in source code to see the main modifications.