riscv-bitmanip/cproofs at master · libraries/riscv-bitmanip · GitHub

Name		Name	Last commit message	Last commit date
parent directory ..
README.md		README.md
bextdep.cc		bextdep.cc
bextdep.sh		bextdep.sh
bit_matrix.cc		bit_matrix.cc
bit_matrix.sh		bit_matrix.sh
bitboards.cc		bitboards.cc
bmi_emulate.cc		bmi_emulate.cc
bmi_emulate.sh		bmi_emulate.sh
clmul.cc		clmul.cc
clmul.py		clmul.py
clmul.sh		clmul.sh
common.h		common.h
examples.cc		examples.cc
examples.sh		examples.sh
fsl_fsr.cc		fsl_fsr.cc
fsl_fsr.sh		fsl_fsr.sh
grevi_pseudo_ops.cc		grevi_pseudo_ops.cc
grevi_pseudo_ops.sh		grevi_pseudo_ops.sh
insns.h		insns.h
misc.cc		misc.cc
misc.sh		misc.sh
printgrev.cc		printgrev.cc
printperm.cc		printperm.cc
printshfl.cc		printshfl.cc
runall.sh		runall.sh
rv_imm_decode.cc		rv_imm_decode.cc
rv_imm_decode.sh		rv_imm_decode.sh
rvintrin.cc		rvintrin.cc
rvintrin.h		rvintrin.h
rvintrin.sh		rvintrin.sh
wops.cc		wops.cc
wops.sh		wops.sh
xperm.cc		xperm.cc
xperm.sh		xperm.sh
zip_unzip.cc		zip_unzip.cc
zip_unzip.sh		zip_unzip.sh

README.md

This directory contains a few proofs for the reference C models used in the RISC-V Bitmanip extension. You need CBMC to run them.