pono
HWMCC’24
Pono ist ein leistungsstarker, anpassungsfähiger und erweiterbarer SMT-basierter Modellprüfer, der in C++ implementiert ist. Es nutzt Smt-Switch, eine generische C++-API für die SMT-Lösung. Pono wurde als nächste Generation von CoSA entwickelt und erhielt daher ursprünglich den Namen cosa2 .
Pono ist das hawaiianische Wort für richtig, korrekt oder gut. Es wird umgangssprachlich oft im moralischen Sinne von „Güte“ oder „Richtigkeit“ verwendet, bezieht sich aber auch auf „richtiges Vorgehen“ oder „Richtigkeit“. Wir verwenden das Wort für mehrere Bedeutungen. Unser Ziel ist es, dass Pono ein nützliches Werkzeug für Menschen sein kann, um die Korrektheit von Systemen zu überprüfen, was sicherlich das Richtige ist.
Pono wurde auf der HWMCC'19 unter seinem ursprünglichen Namen cosa2 mit dem Oski Award für die Lösung der meisten Benchmarks insgesamt ausgezeichnet.
./contrib/setup-bison.sh und ./contrib/setup-flex.sh aus-ly nicht geladen werden kann. Führen Sie in einem solchen Fall das Bison-Setup-Skript aus../contrib/setup-smt-switch.sh aus – es wird smt-switch mit Bitwuzla erstellen./deps/mathsat um--with-msat zum Befehl setup-smt-switch.sh hinzu../contrib/setup-btor2tools.sh aus../configure.sh aus.--with-msat als Option für configure.sh eincd build aus.make .libgmp-static von AUR installieren. Wir verknüpfen mit der gperftools-Bibliothek, um Profilierungsdaten zu generieren. Um die Profilerstellung zu aktivieren, führen Sie ./configure.sh mit dem Flag --with-profiling aus und kompilieren Sie Pono neu, indem Sie make im build -Verzeichnis ausführen. Dies setzt voraus, dass Sie die gperftools-Bibliothek zuvor installiert haben, z. B. führen Sie unter Ubuntu sudo apt-get install google-perftools libgoogle-perftools-dev aus.
Führen Sie zum Profilieren ./pono --profiling-log=<log-file> ... aus, wobei <log-file> der Pfad zu einer Datei ist, in die Profiling-Daten geschrieben werden. Nach normaler oder abnormaler (z. B. durch Senden eines Signals) Beendigung von Pono können die gesammelten Profildaten analysiert werden, indem z. B. google-pprof --text ./pono <log-file> ausgeführt wird, um ein Textprofil zu erstellen. Weitere Optionen finden Sie man google-pprof .
Weitere Informationen zu gperftools finden Sie im Allgemeinen unter https://github.com/gperftools/gperftools/tree/master/docs.
gperftools ist unter einer BSD-3-Klausel-Lizenz lizenziert, siehe https://github.com/gperftools/gperftools/blob/master/COPYING.
Es gibt zwei Transition System-Schnittstellen:
Smt-switch ist eine C++-Solver-agnostische API für SMT-Solver. Das Wichtigste, woran man sich erinnern sollte, ist, dass alles ein Zeiger ist. Objekte können mit using -Anweisungen „typdefiniert“ werden, sie sind aber immer noch shared_ptr s. Wenn Sie also einen Solver oder einen Begriff verwenden, müssen Sie -> Zugriffe verwenden.
Weitere Informationen finden Sie in der Beispielverwendung in den SMT-Switch-Tests. Weitere nützliche Dateien, die Sie besuchen sollten, sind:
smt-switch/include/solver.h : Dies ist die Hauptschnittstelle, die Sie verwenden werdensmt-switch/include/ops.h : Dies enthält alle Operationen, die Sie möglicherweise benötigenOp(Extract, 7, 4) Um die pono -Python-Bindungen zu erstellen, stellen Sie zunächst sicher, dass Sie die Cython-Version >= 0.29 installiert haben. Stellen Sie dann sicher, dass smt-switch und seine Python-Bindungen installiert sind. Abschließend können Sie mit ./configure.sh --python konfigurieren und dann normal erstellen. Die Reihenfolge der Befehle wäre wie folgt:
# 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
Das beste Tool zum Erstellen von BTOR2 aus Verilog ist Yosys. Yosys hat hier ein ausgezeichnetes Handbuch. Sie können yosys auch interaktiv ausführen, indem Sie yosys ohne Argumente ausführen. Anschließend können Sie Hilfemeldungen für jeden Befehl anzeigen mit: help <command> . Wenn Sie help ohne Argumente ausführen, werden alle Befehle aufgelistet.
Ein besonders nützlicher Befehl, wenn Sie Probleme haben, ist show , der den aktuellen Zustand der Schaltung in Yosys anzeigen kann.
Unten finden Sie eine Beispieldatei mit Kommentaren, die jeden Befehl erläutern, der eine BTOR2-Datei für ./samples/counter-false.v erstellt. Dies sollte für die meisten Anwendungsfälle ausreichen.
Sobald Sie yosys installiert haben, kopieren Sie den folgenden Text in gen-btor.ys auf der obersten Ebene dieses Repositorys. Anschließend wird durch Ausführen yosys -s gen-btor.ys die BTOR2-Datei erstellt.
# 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
