Symbolic Processor Verification

This verification approach implementation is based on:

• KLEE
• RISC-V VP
• µrv32---microrv32

Quick Guide

Clone Repo

foo@bar:~$ git clone git@gitlab.informatik.uni-bremen.de:processor_verification/symex_processor_verification.git --recursive

Build Docker Container

foo@bar:~$ make build

Run Docker Container

foo@bar:~$ make run

Build Bytecode / LLVM IR in Docker Container (Optional)

klee@klee:~$ cd src && make bytecode

Run KLEE in Docker Container

klee@klee:~$ cd src && make

How to Cite

Further details are described in the folliwng publication: publication:

@INPROCEEDINGS{nbruns2023symex,
  author={Bruns, Niklas and Herdt, Vladimir and Drechsler, Rolf},
  booktitle={2023 Design, Automation & Test in Europe Conference & Exhibition (DATE)}, 
  title={Processor Verification using Symbolic Execution: A RISC-V Case-Study}, 
  year={2023},
  volume={},
  number={},
  pages={1-6},
  doi={10.23919/DATE56975.2023.10137202}
  }

Acknowledgements

This work was supported in part by the German Federal Ministry of Education and Research (BMBF) within the project Scale4Edge under contract no. 16ME0127, within the project VerSys under contract no. 01IW1900, and within the project ECXL no. 01IW22002.