pono
HWMCC’24
Pono 是一個用 C++ 實現的高效能、適應性強且可擴展的基於 SMT 的模型檢查器。它利用 Smt-Switch，這是一種用於 SMT 解決方案的通用 C++ API。 Pono 是作為下一代 CoSA 開發的，因此最初被命名為cosa2 。
Pono 在夏威夷語中是正確、正確或善良的意思。它經常在口語中用於道德意義上的“善”或“正確”，但也指“適當的程序”或“正確性”。我們使用這個詞有多種含義。我們的目標是 Pono 可以成為人們驗證系統正確性的有用工具，這無疑是正確的事情。
Pono 在 HWMCC'19 上因其解決了最大數量的基準測試而獲得 Oski 獎（原名cosa2） 。
./contrib/setup-bison.sh和./contrib/setup-flex.sh-ly的錯誤。在這種情況下，請執行 bison 安裝腳本。./contrib/setup-smt-switch.sh ——它將使用 Bitwuzla 建構 smt-switch./deps/mathsat--with-msat標誌加入到setup-smt-switch.sh指令中。./contrib/setup-btor2tools.sh 。./configure.sh 。--with-msat作為configure.sh的選項cd build 。make .libgmp-static來修復它。我們連結 gperftools 函式庫來產生分析資料。若要啟用分析，請執行帶有標誌--with-profiling的./configure.sh並透過在build目錄中執行make來重新編譯 Pono。這假設您之前已經安裝了 gperftools 函式庫，例如，在 Ubuntu 上執行sudo apt-get install google-perftools libgoogle-perftools-dev 。
若要進行分析，請執行./pono --profiling-log=<log-file> ...其中<log-file>是寫入分析資料的檔案的路徑。在 Pono 正常或異常（例如透過發送訊號）終止之後，可以透過執行例如google-pprof --text ./pono <log-file>來分析收集的設定檔資料以產生文字設定檔。請參閱man google-pprof以了解更多選項。
一般來說，有關 gperftools 的更多信息，請參閱 https://github.com/gperftools/gperftools/tree/master/docs。
gperftools 依據 BSD 3 條款授權取得許可，請參閱 https://github.com/gperftools/gperftools/blob/master/COPYING。
有兩個過渡系統介面：
Smt-switch 是用於 SMT 求解器的與 C++ 求解器無關的 API。最重要的是要記住，一切都是指針。物件可能是using語句進行「typedef-ed」的，但它們仍然是shared_ptr 。因此，當使用求解器或術語時，您需要使用->存取。
有關更多信息，請參閱 smt-switch 測試中的範例用法。其他需要存取的有用文件包括：
smt-switch/include/solver.h ：這是您將使用的主介面smt-switch/include/ops.h ：這包含您可能需要的所有操作Op(Extract, 7, 4)這樣的索引操作要建立pono python 綁定，首先確保您安裝了 Cython 版本 >= 0.29。然後確保安裝了smt-switch及其 python 綁定。最後可以使用./configure.sh --python進行配置，然後正常建置。命令順序如下：
# 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
從 Verilog 創建 BTOR2 的最佳工具是 Yosys。 Yosys 這裡有一本很棒的手冊。您也可以透過不帶參數來執行 yosys 以互動方式執行 yosys。然後您可以使用以下命令查看每個命令的幫助訊息： help <command> 。不帶參數運行help會列出所有指令。
如果您遇到問題，一個特別有用的指令是show ，它可以顯示 Yosys 中電路的目前狀態。
下面是一個範例文件，其中包含註釋，解釋了為 ./samples/counter-false.v 產生 BTOR2 文件的每個命令。這對於大多數用例來說應該足夠了。
安裝yosys後，將以下文字複製到該儲存庫頂層的gen-btor.ys 。然後，執行yosys -s gen-btor.ys將產生 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
