pono
HWMCC’24
Pono est un vérificateur de modèle basé sur SMT performant, adaptable et extensible implémenté en C++. Il exploite Smt-Switch, une API C++ générique pour la résolution SMT. Pono a été développé comme la prochaine génération de CoSA et s'appelait donc à l'origine cosa2 .
Pono est le mot hawaïen pour bon, correct ou bonté. Il est souvent utilisé familièrement dans le sens moral de « bonté » ou « justice », mais fait également référence à « procédure appropriée » ou à « exactitude ». Nous utilisons le mot dans plusieurs sens. Notre objectif est que Pono puisse être un outil utile permettant aux utilisateurs de vérifier l' exactitude des systèmes, ce qui est sûrement la bonne chose à faire.
Pono a reçu le prix Oski sous son nom d'origine cosa2 au HWMCC'19 pour avoir résolu le plus grand nombre de tests au total.
./contrib/setup-bison.sh et ./contrib/setup-flex.sh-ly . Dans un tel cas, exécutez le script de configuration de bison../contrib/setup-smt-switch.sh -- cela construira smt-switch avec Bitwuzla./deps/mathsat--with-msat à la commande setup-smt-switch.sh ../contrib/setup-btor2tools.sh ../configure.sh .--with-msat comme option pour configure.shcd build .make .libgmp-static depuis AUR. Nous établissons un lien avec la bibliothèque gperftools pour générer des données de profilage. Pour activer le profilage, exécutez ./configure.sh avec l'indicateur --with-profiling et recompilez Pono en exécutant make dans le répertoire build . Cela suppose que vous avez déjà installé la bibliothèque gperftools, par exemple, sur Ubuntu, exécutez sudo apt-get install google-perftools libgoogle-perftools-dev .
Pour créer un profil, exécutez ./pono --profiling-log=<log-file> ... où <log-file> est le chemin d'accès à un fichier dans lequel les données de profilage sont écrites. Après la fin normale ou anormale (par exemple via l'envoi d'un signal) de Pono, les données de profil collectées peuvent être analysées en exécutant, par exemple, google-pprof --text ./pono <log-file> pour produire un profil textuel. Voir man google-pprof pour d'autres options.
En général, voir https://github.com/gperftools/gperftools/tree/master/docs pour plus d'informations sur gperftools.
gperftools est sous licence BSD à 3 clauses, voir https://github.com/gperftools/gperftools/blob/master/COPYING.
Il existe deux interfaces du système de transition :
Smt-switch est une API indépendante du solveur C++ pour les solveurs SMT. La principale chose à retenir est que tout est un indicateur. Les objets peuvent être "typedef-ed" avec des instructions using , mais ils sont toujours shared_ptr s. Ainsi, lorsque vous utilisez un solveur ou un terme, vous devez utiliser les accès -> .
Pour plus d'informations, consultez l'exemple d'utilisation dans les tests smt-switch. D'autres fichiers utiles à visiter incluent :
smt-switch/include/solver.h : c'est l'interface principale que vous utiliserezsmt-switch/include/ops.h : ceci contient toutes les opérations dont vous pourriez avoir besoinOp(Extract, 7, 4) Pour créer les liaisons pono python, assurez-vous d'abord que la version Cython >= 0.29 est installée. Assurez-vous ensuite que smt-switch et ses liaisons python sont installés. Enfin, vous pouvez configurer avec ./configure.sh --python puis construire normalement. La séquence de commandes serait la suivante :
# 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
Le meilleur outil pour créer BTOR2 à partir de Verilog est Yosys. Yosys a un excellent manuel ici. Vous pouvez également exécuter Yosys de manière interactive en exécutant Yosys sans argument. Ensuite, vous pouvez afficher les messages d'aide pour chaque commande avec : help <command> . L'exécution de help sans argument répertorie toutes les commandes.
Une commande particulièrement utile si vous rencontrez des problèmes est show , qui peut afficher l'état actuel du circuit dans Yosys.
Vous trouverez ci-dessous un exemple de fichier avec des commentaires expliquant chaque commande qui produit un fichier BTOR2 pour ./samples/counter-false.v. Cela devrait suffire pour la plupart des cas d’utilisation.
Une fois yosys installé, copiez le texte ci-dessous dans gen-btor.ys au niveau supérieur de ce référentiel. Ensuite, exécuter yosys -s gen-btor.ys produira le fichier 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
