Artifact for ASP-DAC'24 paper: "TIUP: Effective Processor Verification with Tautology-Induced Universal Properties"

Dependencies/Requirements:

git

Packages: sudo apt install git

python 3.6 or later

bison/flex

hw tooling: synthesis suite yosys, symbiyosys, and formal model checker pono

The synthesis suite is used to convert the verilog under verification into the btor2 format used by pono. Pono is a open-source formal model checker. We highly recommend using the freely available oss-cad-suite which can be conveniently downloaded from here. However, it is important to note that the latest version of yosys may not work correctly. Therefore, we have provided the script setup-yosys.sh to compile a specific version of yosys.

If an error occurs during the compilation of yosys, such as error: no member named 'numeric_limits' in namespace 'std' (which may occur in non-Ubuntu 20.04 versions), locate the file yosys/passes/sat/freduce.cc and add the header file #include <limits>.

Download the oss-cad-suite archive matching your OS, then extract it and edit ~/.bashrc:

export OSS_CAD=/path/to/oss-cad-suite/bin
export PATH=$PATH:$OSS_CAD

Set the environment variable:

source ~/.bashrc

Please follow the corresponding README.md and ensure that the yosys, sby, and pono tools are on your $PATH.

You can check this by running (for example): pono --help.

Verification:

We have provided a convenience pushbutton script:

main.py

Which can be invoked with: python3 main.py. To test a specific processor, simply uncomment the corresponding line for that processor, for example: ridecore.verify().

Project structure:

TPV
├── main.py                        # main script to run the verification
├── README.md                      # subscript for every processor         
├── script
│   ├── biriscv
│   ├── picorv32
│   ├── ridecore
│   └── Vscale_plus
├── TPV-Generator                  # the generator of the scheduler
│   ├── constants.vh
│   ├── generate-tpv-files.sh
│   ├── generate_tpv.py
│   ├── LICENSE.v
│   ├── module_interface.py
│   ├── __pycache__
│   ├── scheduler_generator.py
│   ├── scheduler_header.v
│   ├── scheduler.v
│   └── tpv_property.v
├── translateformula               # the translation of the tautologies into the instruction sequence
│   ├── formula.txt                # all tautologies 
│   ├── instructions.txt           # the instruction sequence under verification
│   ├── log.txt
│   ├── Makefile
│   ├── parser.cc
│   ├── parser.hh
│   ├── parser.o
│   ├── parser.output
│   ├── parser.ypp
│   ├── riscv.cpp
│   ├── riscv.h
│   ├── run.sh
│   ├── scanner.lpp
│   ├── tokens.cc
│   ├── tokens.o
│   └── translate.output
├── vlg                            # the source code of the processors under verification
│   ├── biriscv
│   ├── picorv32
│   ├── ridecore
│   └── Vscale_plus
└── setup-yosys.sh                 # script to compile yosys

CrazybinaryLi/TPV