pono

Pono: Pemeriksa Model Berbasis SMT yang Fleksibel dan Dapat Diperluas

Pono adalah pemeriksa model berbasis SMT yang berkinerja, mudah beradaptasi, dan diperluas yang diimplementasikan dalam C++. Ini memanfaatkan Smt-Switch, API C++ generik untuk penyelesaian SMT. Pono dikembangkan sebagai generasi berikutnya dari CoSA dan awalnya diberi nama cosa2 .

Pono adalah kata dalam bahasa Hawaii yang berarti pantas, benar, atau baik. Kata ini sering digunakan dalam bahasa sehari-hari dalam arti moral "kebaikan" atau "kebenaran", tetapi juga merujuk pada "prosedur yang tepat" atau "kebenaran". Kami menggunakan kata tersebut untuk berbagai arti. Tujuan kami adalah agar Pono dapat menjadi alat yang berguna bagi masyarakat untuk memverifikasi kebenaran sistem, yang tentunya merupakan hal yang benar untuk dilakukan.

Publikasi

• Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett: Pono: Pemeriksa Model Berbasis SMT yang Fleksibel dan Dapat Diperluas. CAV 2021.
  • Artefak perangkat lunak yang dievaluasi.
• Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett: Smt-Switch: API C++ Solver-Agnostic untuk Pemecahan SMT. Sabtu 2021.
• Makai Mann: Meningkatkan sistem transisi untuk pemeriksaan model simbolis yang dapat diskalakan. Tesis PhD, Universitas Stanford, 2021.

Penghargaan

Pono dianugerahi Penghargaan Oski dengan nama aslinya cosa2 di HWMCC'19 karena menyelesaikan sejumlah besar tolok ukur secara keseluruhan.

Pengaturan

• [opsional] Pasang bison dan flex
  • Jika Anda belum menginstal bison dan flex secara global, jalankan ./contrib/setup-bison.sh dan ./contrib/setup-flex.sh
  • Meskipun Anda memiliki bison, Anda mungkin mendapatkan kesalahan karena tidak dapat memuat -ly . Jika demikian, jalankan skrip pengaturan bison.
• Jalankan ./contrib/setup-smt-switch.sh -- ini akan membangun smt-switch dengan Bitwuzla
  • [opsional] untuk membangun dengan MathSAT (diperlukan untuk pemeriksaan model berbasis interpolan) Anda perlu mendapatkan perpustakaannya sendiri
    • perhatikan bahwa MathSAT berada di bawah lisensi khusus yang tidak sesuai dengan BSD dan Anda harus memikul semua tanggung jawab untuk memenuhi ketentuan tersebut
    • unduh pemecah dari https://mathsat.fbk.eu/download.html, buka kemasannya dan ganti nama direktori menjadi ./deps/mathsat
    • lalu tambahkan tanda --with-msat ke perintah setup-smt-switch.sh .
• Jalankan ./contrib/setup-btor2tools.sh .
• Jalankan ./configure.sh .
  • jika membangun dengan mathsat, sertakan juga --with-msat sebagai opsi untuk configure.sh
• Jalankan cd build .
• Jalankan make .

Ketergantungan

• Silakan lihat README dari smt-switch untuk dependensi yang diperlukan.
• Catatan untuk pengguna Arch Linux: pembuatan Pono akan gagal jika perpustakaan statis GMP, yang diperlukan oleh cvc5, tidak diinstal pada sistem Anda. Anda dapat memperbaikinya dengan menginstal libgmp-static dari AUR.

Pembuatan profil

Kami menautkan ke perpustakaan gperftools untuk menghasilkan data profil. Untuk mengaktifkan pembuatan profil, jalankan ./configure.sh dengan flag --with-profiling dan kompilasi ulang Pono dengan menjalankan make di direktori build . Ini mengasumsikan bahwa Anda telah menginstal perpustakaan gperftools sebelumnya, misalnya, di Ubuntu, jalankan sudo apt-get install google-perftools libgoogle-perftools-dev .

Untuk membuat profil, jalankan ./pono --profiling-log=<log-file> ... dengan <log-file> adalah jalur ke file tempat data profil ditulis. Setelah penghentian Pono secara normal atau tidak normal (misalnya melalui pengiriman sinyal), data profil yang dikumpulkan dapat dianalisis dengan menjalankan, misalnya, google-pprof --text ./pono <log-file> untuk menghasilkan profil tekstual. Lihat man google-pprof untuk opsi lebih lanjut.

Secara umum, lihat https://github.com/gperftools/gperftools/tree/master/docs untuk informasi lebih lanjut tentang gperftools.

gperftools dilisensikan di bawah lisensi 3-klausul BSD, lihat https://github.com/gperftools/gperftools/blob/master/COPYING.

Kode yang ada

Sistem Transisi

Ada dua antarmuka Sistem Transisi:

• Sistem Transisi Fungsional dalam fts.*
• Sistem Transisi di rts.*

Smt-Beralih

Smt-switch adalah API pemecah-agnostik C++ untuk pemecah SMT. Hal utama yang perlu diingat adalah bahwa segala sesuatu adalah sebuah penunjuk. Objek mungkin "diketik" dengan using pernyataan, tetapi objek tersebut masih shared_ptr . Jadi, saat menggunakan pemecah atau istilah, Anda perlu menggunakan -> akses.

Untuk informasi selengkapnya, lihat contoh penggunaan dalam pengujian smt-switch. File berguna lainnya untuk dikunjungi meliputi:

• smt-switch/include/solver.h : ini adalah antarmuka utama yang akan Anda gunakan
• smt-switch/include/ops.h : ini berisi semua operasi yang mungkin Anda perlukan
  • Catatan: buat operasi yang diindeks seperti Op(Extract, 7, 4)

Ikatan python

Untuk membuat binding pono python, pertama-tama pastikan Anda telah menginstal Cython versi >= 0.29. Kemudian pastikan smt-switch dan binding python-nya telah diinstal. Terakhir, Anda dapat mengonfigurasi dengan ./configure.sh --python lalu membangun secara normal. Urutan perintahnya adalah sebagai berikut:

 # 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

Menghasilkan BTOR2 dari Verilog

Alat terbaik untuk membuat BTOR2 dari Verilog adalah Yosys. Yosys memiliki manual yang bagus di sini. Anda juga dapat menjalankan yosys secara interaktif dengan menjalankan yosys tanpa argumen. Kemudian Anda dapat melihat pesan bantuan untuk setiap perintah dengan: help <command> . Menjalankan help tanpa argumen mencantumkan semua perintah.

Perintah yang sangat berguna jika Anda mengalami masalah adalah show , yang dapat menunjukkan status sirkuit saat ini di Yosys.

Mulai Cepat Yosys

Di bawah ini adalah contoh file dengan komentar yang menjelaskan setiap perintah yang menghasilkan file BTOR2 untuk ./samples/counter-false.v. Ini seharusnya cukup untuk sebagian besar kasus penggunaan.

Setelah Anda menginstal yosys , salin teks di bawah ini ke gen-btor.ys di tingkat atas repositori ini. Kemudian, menjalankan yosys -s gen-btor.ys akan menghasilkan file 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