Skip to content

Latest commit

 

History

History
69 lines (49 loc) · 2.09 KB

README.md

File metadata and controls

69 lines (49 loc) · 2.09 KB

Five

Five is a standalone implementation of the classic five-stage processor pipeline that can be understood and formally verified independently of the instruction-set implementation. Separately, we provide a RISC-V microcontroller called FiveAlive that demonstrates use of the pipeline in an actual processor core. Five is written in Blarney.

Dependencies

First, download the repo:

git clone --recursive https://github.com/blarney-lang/five

We then have the following dependencies:

  • GHC (version 9.4.5 known working)
  • The z3 solver (version 4.12.2 known working)
  • SymbiYosys OSS CAD Suite (version 2024-11-27 known working)

If you have trouble meeting any of the dependencies, you can simply enter a docker shell:

make shell

Usage

The pipeline can be verified either via SymbiYosys or the z3 SMT solver.

Verilog and SMT files for verification can be generated as follows.

make gen

The outputs are written to the gen/ directory and can be checked as follows.

cd gen
sby Correctness.sby -f       # Check using SymbiYosys
sby ForwardProgress.sby -f   # Check using SymbiYosys
z3 Correctness.smt2          # Check using z3
z3 ForwardProgress.smt2      # Check using z3

If z3 is in your PATH then the following command can be used.

make verify

For unbounded checking, which requires around ten hours to complete, the following command can be used.

make verify-unbounded

Acknowledgements

Thanks to Alexandre Joannou and Victor Miquel for their contributions to Blarney's SMT backend, which allowed verification of all pipeline properties. Five was developed on the CAPcelerate project, part of the UKRI's Digital Security by Design programme.