| FazBrowse GitHub Viewer | Trending | | Home |
| Tools: [Download Repo ZIP] [Original HTTPS Page] |
| Name | Name | Last commit date | ||
|---|---|---|---|---|
PyCaliper provides infrastructure for verifying and synthesizing specifications for RTL designs based on the Caliper specification language.
PyCaliper has been developed and tested with Python 3.11. We recommend using a virtual-environment. PyCaliper can be run without building (see [no-build] below) or by building the package (see [install] below).
git clone https://github.com/pycaliper/pycaliper.git
git clone https://github.com/pycaliper/btor2ex.gitpip install -r requirements.txtexport PYTHONPATH=$PYTHONPATH:$(pwd)/pycaliper
export PYTHONPATH=$PYTHONPATH:$(pwd)/btor2excd pycaliper
python3 -m tests.testgit clone https://github.com/pycaliper/pycaliper.git
git clone https://github.com/pycaliper/btor2ex.gitcd <path to pycaliper>
pip install .
cd <path to btor2ex>
pip install .The quickstart.py script provides a simple example of how to use PyCaliper. It checks the design from the examples/designs/demo directory. It uses the PyCaliper demos specification from the tests/specs/demo.py file.
python quickstart.pyThis examples uses the BTOR backend (using the btor2ex package) to check the design. PyCaliper also supports the Jasper backend.
Run the main script (after installing PyCaliper) to see the available commands:
$ pycaliper --help
Usage: pycaliper [OPTIONS] COMMAND [ARGS]...
PyCaliper: Specification Synthesis and Verification Infrastructure.
╭─ Options ───────────────────────────────────────────────────────────────────────────────────────────────────────╮
│ --install-completion Install completion for the current shell. │
│ --show-completion Show completion for the current shell, to copy it or customize the installation. │
│ --help Show this message and exit. │
╰─────────────────────────────────────────────────────────────────────────────────────────────────────────────────╯
╭─ Commands ──────────────────────────────────────────────────────────────────────────────────────────────────────╮
│ persynth Synthesize invariants using Partial Equivalence Relations (PER). │
│ svagen Generate SystemVerilog Assertions (SVA) from a PyCaliper specification. │
│ verif Verify invariants in a PyCaliper specification. │
╰─────────────────────────────────────────────────────────────────────────────────────────────────────────────────╯We provide a documentation site for PyCaliper.
The PyCaliper project welcomes external contributions through pull requests to the main branch.
We use pre-commit, so before contributing, please ensure that you run pre-commit and make sure all checks pass with
pre-commit install pre-commit run --all-files
Please also run the provided tests and add further tests targetting newly contributed features.
We encourage feedback and suggestions via GitHub Issues.
| Back | FazBrowse Home | New Git URL |