pono
HWMCC’24
Pono é um verificador de modelo baseado em SMT de desempenho, adaptável e extensível implementado em C++. Ele aproveita o Smt-Switch, uma API C++ genérica para resolução de SMT. Pono foi desenvolvido como a próxima geração do CoSA e, portanto, foi originalmente denominado cosa2 .
Pono é a palavra havaiana para adequado, correto ou bondade. É frequentemente usado coloquialmente no sentido moral de "bondade" ou "correção", mas também se refere a "procedimento adequado" ou "correção". Usamos a palavra para vários significados. Nosso objetivo é que o Pono possa ser uma ferramenta útil para as pessoas verificarem a exatidão dos sistemas, o que certamente é a coisa certa a fazer.
Pono recebeu o Prêmio Oski com seu nome original cosa2 no HWMCC'19 por resolver o maior número de benchmarks gerais.
./contrib/setup-bison.sh e ./contrib/setup-flex.sh-ly . Nesse caso, execute o script de configuração do bison../contrib/setup-smt-switch.sh - ele construirá smt-switch com Bitwuzla./deps/mathsat--with-msat ao comando setup-smt-switch.sh ../contrib/setup-btor2tools.sh ../configure.sh .--with-msat como uma opção para configure.shcd build .make .libgmp-static do AUR. Vinculamos à biblioteca gperftools para gerar dados de perfil. Para habilitar a criação de perfil, execute ./configure.sh com flag --with-profiling e recompile o Pono executando make no diretório build . Isso pressupõe que você tenha instalado a biblioteca gperftools antes, por exemplo, no Ubuntu, execute sudo apt-get install google-perftools libgoogle-perftools-dev .
Para criar um perfil, execute ./pono --profiling-log=<log-file> ... onde <log-file> é o caminho para um arquivo onde os dados de criação de perfil são gravados. Após o encerramento normal ou anormal (por exemplo, através do envio de um sinal) do Pono, os dados do perfil coletados podem ser analisados executando, por exemplo, google-pprof --text ./pono <log-file> para produzir um perfil textual. Consulte man google-pprof para obter mais opções.
Em geral, consulte https://github.com/gperftools/gperftools/tree/master/docs para obter mais informações sobre gperftools.
gperftools é licenciado sob uma licença BSD de 3 cláusulas, consulte https://github.com/gperftools/gperftools/blob/master/COPYING.
Existem duas interfaces do Sistema de Transição:
Smt-switch é uma API independente de solucionador C++ para solucionadores SMT. A principal coisa a lembrar é que tudo é um ponteiro. Os objetos podem ser "typedef-ed" com instruções using , mas ainda são shared_ptr s. Assim, ao usar um solucionador ou um termo, você precisa usar -> acessos.
Para obter mais informações, consulte o exemplo de uso nos testes smt-switch. Outros arquivos úteis para visitar incluem:
smt-switch/include/solver.h : esta é a interface principal que você usarásmt-switch/include/ops.h : contém todas as operações que você pode precisarOp(Extract, 7, 4) Para construir as ligações pono python, primeiro certifique-se de ter a versão Cython >= 0.29 instalada. Em seguida, certifique-se de que smt-switch e suas ligações python estejam instaladas. Finalmente, você pode configurar com ./configure.sh --python e então construir normalmente. A sequência de comandos seria a seguinte:
# 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
A melhor ferramenta para criar BTOR2 da Verilog é o Yosys. Yosys tem um excelente manual aqui. Você também pode executar o yosys interativamente executando o yosys sem argumentos. Então você pode visualizar mensagens de ajuda para cada comando com: help <command> . Executar help sem argumentos lista todos os comandos.
Um comando particularmente útil se você estiver com problemas é show , que pode mostrar o estado atual do circuito no Yosys.
Abaixo está um arquivo de exemplo com comentários explicando cada comando que produz um arquivo BTOR2 para ./samples/counter-false.v. Isso deve ser suficiente para a maioria dos casos de uso.
Depois de instalar yosys , copie o texto abaixo em gen-btor.ys no nível superior deste repositório. Então, executar yosys -s gen-btor.ys produzirá o arquivo 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
