PipeSynth is a methology and automated tool for synthesizing microarchitectural ordering axioms from small programs (litmus tests) and execution traces.
If you use our tool in your work, we would appreciate it if you cite our paper(s):
Chase Norman, Adwait Godbole, and Yatin A. Manerkar. "PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency", 28th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2023.
If you have any comments, questions, or feedback, please contact Yan-Ru Jhou (yanruj at umich dot edu), Yatin Manerkar (manerkar at umich dot edu), or visit our GitHub page, https://github.com/chasenorman/PipeSynth-AEC.
At this point, PipeSynth is a research tool rather than an industry-strength synthesis toolchain. We do appreciate any suggestions or feedback either in approach or in implementation. If you are interested in any particular feature, missing item, or implementation detail, please contact the authors and we will try to help out as best we can.
PipeSynth is written in Python and uses the CVC5 SMT solver to generate the first-order microarchitectural ordering axioms. PipeSynth requires Python 3.8 (or later), and CVC5 (0.0.4 for python api and 1.0.2 for SyGuS solving) The authors have compiled and executed PipeSynth successfully on MacOS.
PipeSynth uses a number of tools and libraries.
Download cvc5-0.0.4 Source Code
# change the directory to the source code folder
# build cvc5 0.0.4
./configure.sh --python-bindings --auto-download
cd build
# use -jN for parallel build with N threads
make
# install cvc5 0.0.4
sudo make install
sudo cp -r ./build/lib/* $( python -c 'import sysconfig; print(sysconfig.get_paths()["purelib"])')
Basic Usage:
# For uarch vscale, we generate SyGuS files by replacing po_fetch axiom with fifo templates
python3 main.py vscale po_fetch fifo
# Run CVC5 1.0.2 to solve generated SyGuS files
./benchmark
The SyGuS files will appear in the out/ directory. The benchmark script
will run all SyGuS files in the directory and write to a file
out/results.txt
with synthesis results and times.
python3 main.py fivestage all
python3 main.py vscale writes3 writes reads totalorderondx fifo
python3 main.py fivestageoooslr writes path fifo
PipeSynth is an automated formal methodology and tool for the pre-RTL formal synthesis of microarchitectural ordering axioms in the domain specific µspec language. Given a partial µspec ordering specification, litmus tests, and observable execution traces, PipeSynth can automatically synthesise additional µspec ordering axioms that are necessary to guarantee correctness for the provided tests and traces. PipeSynth thus helps architects and hardware engineers automatically generate formal ordering specifications for their microarchitectures even if they do not have prior formal methods expertise. In doing so, it will enable the increased use of formal verification for emerging microarchitectures. This will help catch bugs faster and substantially improve the correctness of the processors of tomorrow.
For building CVC5:
Q: When run ./configure.sh --python-bindings --auto-download
, it shows -- Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS)
error message
A: Add -DPYTHON_INCLUDE_DIR=$(python -c "import sysconfig; print(sysconfig.get_path('include'))")
and -DPYTHON_LIBRARY=$(python -c "import sysconfig; print(sysconfig.get_config_var('LIBDIR'))")
in the configure.sh .