pono
HWMCC’24
Pono — это производительная, адаптируемая и расширяемая программа проверки моделей на основе SMT, реализованная на C++. Он использует Smt-Switch, универсальный API C++ для SMT-решений. Pono был разработан как следующее поколение CoSA и поэтому первоначально назывался cosa2 .
Поно — это гавайское слово, означающее «правильный», «правильный» или «добрый». В разговорной речи оно часто используется в моральном смысле «доброта» или «правильность», но также относится и к «правильной процедуре» или «правильности». Мы используем это слово в нескольких значениях. Наша цель состоит в том, чтобы Pono мог стать для людей полезным инструментом для проверки правильности систем, что, безусловно, правильно .
Pono был награжден премией Oski Award под своим первоначальным названием cosa2 на HWMCC'19 за решение наибольшего количества тестов в целом.
./contrib/setup-bison.sh и ./contrib/setup-flex.sh-ly . В таком случае запустите сценарий установки Bison../contrib/setup-smt-switch.sh — он создаст smt-switch с помощью Bitwuzla../deps/mathsat--with-msat в команду setup-smt-switch.sh ../contrib/setup-btor2tools.sh ../configure.sh .--with-msat в качестве опции в configure.shcd build .make .libgmp-static из AUR. Мы связываемся с библиотекой gperftools для создания данных профилирования. Чтобы включить профилирование, запустите ./configure.sh с флагом --with-profiling и перекомпилируйте Pono, запустив make в каталоге build . Предполагается, что вы уже установили библиотеку gperftools, например, в Ubuntu, запустите sudo apt-get install google-perftools libgoogle-perftools-dev .
Для профилирования запустите ./pono --profiling-log=<log-file> ... где <log-file> — это путь к файлу, в который записываются данные профилирования. После нормального или ненормального (например, посредством отправки сигнала) завершения Pono собранные данные профиля можно проанализировать, запустив, например, google-pprof --text ./pono <log-file> для создания текстового профиля. Дополнительные параметры см. в man google-pprof .
В общем, дополнительную информацию о gperftools см. на https://github.com/gperftools/gperftools/tree/master/docs.
gperftools лицензируется по лицензии BSD с 3 пунктами, см. https://github.com/gperftools/gperftools/blob/master/COPYING.
Существует два интерфейса системы перехода:
Smt-switch — это независимый от решателя C++ API для решателей SMT. Главное помнить, что все является указателем. Объекты могут быть «описаны по типу» с помощью операторов using , но они по-прежнему являются объектами shared_ptr ». Таким образом, при использовании решателя или термина вам необходимо использовать -> доступы.
Для получения дополнительной информации см. пример использования в тестах smt-switch. Другие полезные файлы для посещения:
smt-switch/include/solver.h : это основной интерфейс, который вы будете использовать.smt-switch/include/ops.h : содержит все операции, которые могут вам понадобиться.Op(Extract, 7, 4) Чтобы создать привязки pono Python, сначала убедитесь, что у вас установлена версия Cython >= 0.29. Затем убедитесь, что smt-switch и его привязки Python установлены. Наконец, вы можете настроить с помощью ./configure.sh --python , а затем выполнить сборку в обычном режиме. Последовательность команд будет следующей:
# Optional recommended step: start a python virtualenv
# If you install in the virtualenv, you will need to activate it each time before using pono
# and deactivate the virtualenv with: deactivate
python3 -m venv env
source ./env/bin/activate
pip install Cython==0.29 pytest
./contrib/setup-smt-switch.sh --python
./contrib/setup-btor2tools.sh
pip install -e ./deps/smt-switch/build/python
./configure.sh --python
cd build
make -j4
pip install -e ./python
cd ../
# Test the bindings
pytest ./tests
Лучшим инструментом для создания BTOR2 из Verilog является Yosys. У Yosys есть отличное руководство. Вы также можете запустить yosys в интерактивном режиме, запустив yosys без аргументов. Затем вы можете просмотреть справочные сообщения для каждой команды с помощью: help <command> . При запуске help без аргументов выводятся все команды.
Если у вас возникли проблемы, особенно полезна команда show , которая может показать текущее состояние схемы в Yosys.
Ниже приведен пример файла с комментариями, объясняющими каждую команду, создающую файл BTOR2 для ./samples/counter-false.v. Этого должно быть достаточно для большинства случаев использования.
После установки yosys скопируйте приведенный ниже текст в gen-btor.ys верхнего уровня этого репозитория. Затем запуск yosys -s gen-btor.ys создаст файл BTOR2.
# read in the file(s) -- there can be multiple
# whitespace separated files, and you can
# escape new lines if necessary
read -formal ./samples/counter-false.v;
# prep does a conservative elaboration
# of the top module provided
prep -top counter;
# this command just does a sanity check
# of the hierarchy
hierarchy -check;
# If an assumption is flopped, you might
# see strange behavior at the last state
# (because the clock hasn't toggled)
# this command ensures that assumptions
# hold at every state
chformal -assume -early;
# this processes memories
# nomap means it will keep them as arrays
memory -nomap;
# flatten the design hierarchy
flatten;
# (optional) uncomment and set values to simulate reset signal
# use -resetn for an active low pin
# -n configures the number of cycles to simulate
# -rstlen configures how long the reset is active (recommended to keep it active for the whole simulation)
# -w tells it to write back the final state of the simulation as the initial state in the btor2 file
# another useful option is -zinit which zero initializes any uninitialized state
# sim -clock <clockpin> -reset <resetpin> -n <number of cycles> -rstlen <number of cycles> -w <top_module>
# (optional) use an "explicit" clock
# e.g. every state is a half cycle of the
# fastest clock
# use this option if you see errors that
# refer to "adff" or asynchronous components
# IMPORTANT NOTE: the clocks are not
# automatically toggled if you use this option
# clk2fflogic;
# This turns all undriven signals into
# inputs
setundef -undriven -expose;
# This writes to a file in BTOR2 format
write_btor counter-false.btor2
