pono
HWMCC’24
Pono es un verificador de modelos basado en SMT eficaz, adaptable y extensible implementado en C++. Aprovecha Smt-Switch, una API genérica de C++ para resolución SMT. Pono se desarrolló como la próxima generación de CoSA y por eso originalmente se llamó cosa2 .
Pono es la palabra hawaiana que significa apropiado, correcto o bondad. A menudo se usa coloquialmente en el sentido moral de "bondad" o "rectitud", pero también se refiere a "procedimiento adecuado" o "corrección". Usamos la palabra con múltiples significados. Nuestro objetivo es que Pono pueda ser una herramienta útil para que las personas verifiquen la corrección de los sistemas, lo que seguramente es lo correcto .
Pono recibió el premio Oski bajo su nombre original cosa2 en HWMCC'19 por resolver la mayor cantidad de puntos de referencia en general.
./contrib/setup-bison.sh y ./contrib/setup-flex.sh-ly . En tal caso, ejecute el script de configuración de bison../contrib/setup-smt-switch.sh : compilará smt-switch con Bitwuzla./deps/mathsat--with-msat al comando setup-smt-switch.sh ../contrib/setup-btor2tools.sh ../configure.sh .--with-msat como una opción para configure.shcd build .make .libgmp-static desde AUR. Nos vinculamos con la biblioteca gperftools para generar datos de perfiles. Para habilitar la creación de perfiles, ejecute ./configure.sh con el indicador --with-profiling y vuelva a compilar Pono ejecutando make en el directorio build . Esto supone que ha instalado la biblioteca gperftools antes, por ejemplo, en Ubuntu, ejecute sudo apt-get install google-perftools libgoogle-perftools-dev .
Para crear un perfil, ejecute ./pono --profiling-log=<log-file> ... donde <log-file> es la ruta a un archivo donde se escriben los datos de perfil. Después de la terminación normal o anormal (por ejemplo, mediante el envío de una señal) de Pono, los datos del perfil recopilados se pueden analizar ejecutando, por ejemplo, google-pprof --text ./pono <log-file> para producir un perfil textual. Consulte man google-pprof para obtener más opciones.
En general, consulte https://github.com/gperftools/gperftools/tree/master/docs para obtener más información sobre gperftools.
gperftools tiene una licencia BSD de 3 cláusulas, consulte https://github.com/gperftools/gperftools/blob/master/COPYING.
Hay dos interfaces del sistema de transición:
Smt-switch es una API independiente del solucionador de C++ para solucionadores SMT. Lo principal que hay que recordar es que todo es un puntero. Los objetos pueden ser "typedef-ed" con declaraciones using , pero siguen siendo shared_ptr s. Por lo tanto, cuando utilice un solucionador o un término, deberá utilizar -> accesos.
Para obtener más información, consulte el ejemplo de uso en las pruebas de smt-switch. Otros archivos útiles para visitar incluyen:
smt-switch/include/solver.h : esta es la interfaz principal que utilizarásmt-switch/include/ops.h : contiene todas las operaciones que puedas necesitarOp(Extract, 7, 4) Para construir los enlaces de pono python, primero asegúrese de tener instalada la versión de Cython >= 0.29. Luego asegúrese de que smt-switch y sus enlaces de Python estén instalados. Finalmente, puede configurar con ./configure.sh --python y luego compilar normalmente. La secuencia de comandos sería la siguiente:
# 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
La mejor herramienta para crear BTOR2 desde Verilog es Yosys. Yosys tiene un excelente manual aquí. También puedes ejecutar yosys de forma interactiva ejecutando yosys sin argumentos. Luego podrá ver los mensajes de ayuda para cada comando con: help <command> . Al ejecutar help sin argumentos se enumeran todos los comandos.
Un comando particularmente útil si tienes problemas es show , que puede mostrar el estado actual del circuito en Yosys.
A continuación se muestra un archivo de ejemplo con comentarios que explican cada comando que produce un archivo BTOR2 para ./samples/counter-false.v. Esto debería ser suficiente para la mayoría de los casos de uso.
Una vez que haya instalado yosys , copie el texto a continuación en gen-btor.ys en el nivel superior de este repositorio. Luego, ejecutar yosys -s gen-btor.ys producirá el archivo 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
