INSTALL.adoc

Installation Instructions

Table of Contents

• 1. Dependencies
  • 1.1. Dependencies for building the model
  • 1.2. Dependencies for compiling the tests
  • 1.3. Dependencies for running the Kami-generated Verilog model on riscv-tests
• 2. Repositories needed to build the model
• 3. Repository needed to run riscv-tests
• 4. Ubuntu-specific instructions
  • 4.1. One time installation
  • 4.2. Cloning the model.
  • 4.3. Building and running the riscv-tests

1. Dependencies

1.1. Dependencies for building the model

1. Coq 8.11.0

2. GHC 8.6.5 or newer and Cabal

1.2. Dependencies for compiling the tests

1. RISCV GCC 8.2.0-2019.02.0

1.3. Dependencies for running the Kami-generated Verilog model on riscv-tests

1. Clang 3.8.0 or newer

2. Verilator master branch (4.015 devel rev UNKNOWN_REV)

Note that the versions mentioned above are known to work. Try other versions at your own peril. In particular, GHC 8.2.2 or newer works; Clang 10.0.0 or newer works but Clang 8.0.0 does not work; Verilator 4.013 devel rev UNKNOWN_REV or newer works.

2. Repositories needed to build the model

• RiscvSpecFormal: The top level repository containing the actual model in sub repositories along with several scripts for building and running https://github.com/sifive/RiscvSpecFormal

  • FpuKami: The formal specification of IEEE floating point standard (IEEE 754) in Kami and an implementation in Kami https://github.com/sifive/FpuKami

  • Kami: The Coq-based DSL + tactics + theorems to write and prove hardware in Coq https://github.com/sifive/Kami

  • ProcKami: The formal specification of RISCV-ISA written in Kami https://github.com/sifive/ProcKami

  • StdLibKami: The standard library of useful Kami modules https://github.com/sifive/StdLibKami

  • bbv: The bitvector library from MIT (stands for Bedrock Bit Vectors) https://github.com/mit-plv/bbv

  • coq-record-updates: Utility library for in-place updates of Coq (Gallina) records https://github.com/tchajed/coq-record-update

3. Repository needed to run riscv-tests

• riscv-tests: https://github.com/riscv/riscv-tests

4. Ubuntu-specific instructions

Note that in the following set of instructions sudo permission is needed to install the tools from Ubuntu’s official repositories and other PPAs. One can also install these packages directly from sources without sudo permission. Please refer to the specific packages websites for instructions on how to do it. If the following instructions are followed one after the other, one should be able to build the model and run most of the tests in riscv-tests (the instructions for running the tests are also provided).

4.1. One time installation

4.1.1. Always necessary

Installing Coq

sudo add-apt-repository ppa:jgross-h/many-coq-versions --yes
sudo apt-get update
sudo apt-get install coq-8.10.0 --yes
coqc --version

Installing GHC and Cabal

Note that this PPA installs ghc in a non-standard location ($HOME/.ghcup/bin) so as to not clobber your existing ghc installation.

export BOOTSTRAP_HASKELL_NONINTERACTIVE=1
curl https://get-ghcup.haskell.org -sSf | sh
source $HOME/.ghcup/env
ghc --version
cabal --version

Installing RISCV GCC

These instructions install RISCV GCC on the current directory and adds that directory to the path for later commands to execute correctly.

wget https://static.dev.sifive.com/dev-tools/riscv64-unknown-elf-gcc-8.2.0-2019.02.0-x86_64-linux-ubuntu14.tar.gz
tar xzf riscv64-unknown-elf-gcc-8.2.0-2019.02.0-x86_64-linux-ubuntu14.tar.gz
export PATH=`pwd`/riscv64-unknown-elf-gcc-8.2.0-2019.02.0-x86_64-linux-ubuntu14/bin:$PATH
riscv64-unknown-elf-gcc --version

Installing RISCV tests

riscv-tests will be installed in riscv-tests-install.

git clone https://github.com/riscv/riscv-tests
cd riscv-tests
git submodule update --init --recursive
autoconf
./configure --prefix=`pwd`/../riscv-tests-install
make -j && make install
cd ..

4.1.2. Necessary for generating the Verilog model generated from Kami

Installing Clang

sudo apt-get install clang --yes
clang --version

Installing Verilator

Verilator will be install inside the directory verilator-binary, which will be added to the path.

git clone http://git.veripool.org/git/verilator
cd verilator
autoconf
./configure --prefix=`pwd`/../verilator-binary
make -j 4 && make install
export PATH=`pwd`/../verilator-binary/bin:$PATH
verilator --version
cd ..

4.1.3. Necessary for generating the Haskell model generated from Kami

Installing Cabal packages

cabal update
cabal install hashmap
cabal install vector
cabal install bv
cabal install random
cabal install primitive

4.2. Cloning the model.

git clone https://github.com/sifive/RiscvSpecFormal.git
cd RiscvSpecFormal
git submodule update --init

4.3. Building and running the riscv-tests

The following command builds the model and runs the riscv-tests. runTests.sh requires the path of the directory where riscv-tests are installed.

4.3.1. Running the 32-bit tests on the Verilog model generated from Kami

./runTests.sh --path `pwd`/../riscv-tests/isa --xlen 32

4.3.2. Running the 64-bit tests on the Verilog model generated from Kami

./runTests.sh --path `pwd`/../riscv-tests/isa --xlen 64

4.3.3. Running the 32-bit tests on the Haskell model generated from Kami

./runTests.sh --path `pwd`/../riscv-tests/isa --haskell-sim --xlen 32

4.3.4. Running the 64-bit tests on the Haskell model generated from Kami

./runTests.sh --path `pwd`/../riscv-tests/isa --haskell-sim --xlen 64